Theorems · Inductive type · group theory
CommSemigroup
Type u → Type u
A commutative semigroup is a type with an associative commutative (*).
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 62 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 by101
Results whose statement or proof uses this declaration.
- mul_left_commstatement and proof · cited by 184
- mul_right_commstatement and proof · cited by 108
- mul_mul_mul_commstatement and proof · cited by 65
- dvd_mul_leftstatement and proof · cited by 47
- dvd_mul_of_dvd_rightstatement and proof · cited by 29
- mul_dvd_mulstatement and proof · cited by 24
- Set.commMonoidproof · cited by 21
- Dvd.intro_leftstatement and proof · cited by 20
- Dvd.dvd.mul_leftstatement · cited by 14
- dvd_of_mul_left_eqstatement · cited by 14
- mul_rotatestatement and proof · cited by 12
- Set.center_eq_univstatement and proof · cited by 10