Theorems · Inductive type · group theory
CancelCommMonoid
Type u → Type u
Commutative version of CancelMonoid.
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 23 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 by32
Results whose statement or proof uses this declaration.
- Finset.prod_sdiff_eq_prod_sdiff_iffstatement and proof · cited by 2
- mulRothNumber_map_mul_leftstatement and proof · cited by 1
- eq_iff_eq_of_mul_eq_mulstatement and proof · cited by 1
- Monoid.exponent_eq_max'_orderOfstatement and proof · cited by 1
- Finset.card_Ico_mul_rightstatement and proof · cited by 1
- CancelCommMonoid.casesOnstatement and proof · cited by 1
- CancelCommMonoid.extstatement and proof · cited by 1
- IsMulFreimanHom.monostatement and proof · cited by 1
- isMulFreimanHom_antitonestatement and proof · cited by 1
- CancelCommMonoid.toCommMonoid_injectivestatement and proof · cited by 1
- Set.MulAntidiagonal.finite_of_isWFstatement and proof · cited by 0
- mulRothNumber_map_mul_rightstatement and proof · cited by 0