Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
dedekind::algebra::IsGroup Concept Referenceexport
module dedekind.algebra

Proposition: a set object X whose carrier X::Domain forms a group — the set-indexed lift of category::IsGroup. More...

Concept definition

template<typename X, typename Op std::plus<typename X::Domain>>
concept dedekind::algebra::IsGroup = IsAlgebraOnSet<X, Op> &&
dedekind::category::IsGroup<typename X::Domain, Op>
dedekind::algebra::IsAlgebraOnSet
An algebraic set: a Tarski set whose carrier is closed under a family of operations....
Definition universal.cppm:187
dedekind::algebra::IsGroup
Proposition: a set object X whose carrier X::Domain forms a group — the set-indexed lift of category:...
Definition group.cppm:227
dedekind::category::IsGroup
A Monoid with two-sided Inverses (The Perfect Symmetry).
Definition total.cppm:624

Detailed Description

Proposition: a set object X whose carrier X::Domain forms a group — the set-indexed lift of category::IsGroup.

X is an ETCS set, its carrier X::Domain satisfies the axiomatic category::IsGroup<X::Domain, Op>, and IsAlgebraOnSet supplies the carrier discipline (IsLSet roots std::semiregular on X::Domain, IsClosedAlgebra pins strict closure). The Op-defaulted IsAdditiveGroup / IsMultiplicativeGroup siblings name the canonical additive / multiplicative witnesses.

Template Parameters
XThe set object (category::IsSet).
OpThe binary operation on X::Domain (defaults to std::plus).