Module un_algebra::group::add_group

Additive groups.

An algebraic additive group is an additive monoid M, where each group element g has a unique additive inverse element denoted -g. The inverse operation is called negation.

Axioms

∀g, 0 ∈ M

Inverse: ∃-g ∈ M: g + -g = -g + g = 0.

References

See references for a formal definition of an additive group.

Traits

AddGroup	An algebraic additive group.
AddGroupLaws	Laws of additive groups.
NumAddGroupLaws	Numeric laws of additive groups.