Theorems · Inductive type · group theory
AddCancelCommMonoid
Type u → Type u
Commutative version of AddCancelMonoid.
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 48 results in Mathlib
- Foundations
- Depth 0 from the axioms · 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 by62
Results whose statement or proof uses this declaration.
- AddCommGroup.ModEq.add_iff_leftstatement and proof · cited by 3
- addRothNumber_map_add_leftstatement and proof · cited by 3
- Derivation.mk'statement and proof · cited by 3
- HahnSeries.addValstatement and proof · cited by 3
- Finset.pairwiseDisjoint_piAntidiag_map_addRightEmbeddingstatement and proof · cited by 3
- Finset.piAntidiag_consstatement and proof · cited by 2
- Finset.sum_sdiff_eq_sum_sdiff_iffstatement and proof · cited by 2
- StrictConvexOn.translate_rightstatement and proof · cited by 2
- AddCommGroup.ModEq.add_iff_rightstatement and proof · cited by 1
- isAddFreimanHom_antitonestatement and proof · cited by 1
- AddCommGroup.ModEq.add_left_cancelstatement and proof · cited by 1
- AddCommGroup.ModEq.add_right_cancelstatement and proof · cited by 1