Theorems · Inductive type · group theory
AddGroup
Type u → Type u
An AddGroup is an AddMonoid with a unary - satisfying -a + a = 0.
There is also a binary operation - such that a - b = a + -b,
with a default so that a - b = a + -b holds by definition.
Use AddGroup.ofLeftAxioms or AddGroup.ofRightAxioms to define an
additive group structure on a type with the minimum proof obligations.
[Wikidata Q83478](https://www.wikidata.org/wiki/Q83478)
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 4,410 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by5,135
Results whose statement or proof uses this declaration.
- AddSubgroupstatement · cited by 3,232
- absstatement and proof · cited by 1,814
- AddTorsorstatement · cited by 1,657
- IsTopologicalAddGroupstatement · cited by 1,394
- sub_selfstatement and proof · cited by 996
- map_substatement and proof · cited by 565
- AddSubgroup.zmultiplesstatement and proof · cited by 493
- sub_eq_zerostatement and proof · cited by 407
- map_negstatement and proof · cited by 378
- QuotientAddGroup.mkstatement and proof · cited by 348
- sub_add_cancelstatement and proof · cited by 344
- IsUniformAddGroupstatement · cited by 342
Showing the 200 most cited of 5,135.