Theorems · Inductive type · group theory
Semigroup
Type u → Type u
A semigroup is a type with an associative (*).
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 202 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 by308
Results whose statement or proof uses this declaration.
- mul_assocstatement and proof · cited by 1,667
- SemigroupAction.mul_smulstatement and proof · cited by 291
- Dvd.dvd.transstatement · cited by 148
- dvd_mul_rightstatement and proof · cited by 89
- dvd_transstatement and proof · cited by 50
- map_dvdstatement and proof · cited by 44
- DecompositionMonoidstatement · cited by 39
- mul_dvd_mul_leftstatement and proof · cited by 34
- Dvd.introstatement and proof · cited by 26
- dvd_addstatement and proof · cited by 25
- dvd_mul_of_dvd_leftstatement and proof · cited by 25
- Set.monoidproof · cited by 19
Showing the 200 most cited of 308.