Theorems · Inductive type · group theory
AddCommSemigroup
Type u → Type u
A commutative additive semigroup is a type with an associative commutative (+).
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 178 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 by208
Results whose statement or proof uses this declaration.
- add_tsub_cancel_rightstatement and proof · cited by 172
- tsub_add_cancel_of_lestatement and proof · cited by 112
- add_right_commstatement and proof · cited by 85
- add_tsub_cancel_of_lestatement and proof · cited by 79
- add_left_commstatement and proof · cited by 76
- add_add_add_commstatement and proof · cited by 56
- add_tsub_cancel_leftstatement and proof · cited by 42
- tsub_le_iff_leftstatement and proof · cited by 38
- Set.addCommMonoidproof · cited by 25
- tsub_add_eq_add_tsubstatement and proof · cited by 23
- tsub_le_tsubstatement and proof · cited by 18
- add_tsub_assoc_of_lestatement and proof · cited by 16
Showing the 200 most cited of 208.