Theorems · Inductive type · group theory
IsLeftCancelMulZero
(M₀ : Type u) → [Mul M₀] → [Zero M₀] → Prop
A mixin for left cancellative multiplication by nonzero elements.
- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Cited by
- 48 results in Mathlib
- Foundations
- Depth 1 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 by59
Results whose statement or proof uses this declaration.
- mul_right_inj'statement and proof · cited by 56
- mul_left_cancel₀statement and proof · cited by 47
- associated_of_dvd_dvdstatement and proof · cited by 28
- mul_dvd_mul_iff_leftstatement and proof · cited by 24
- mul_right_injective₀statement and proof · cited by 20
- dvd_antisymm_of_normalize_eqstatement and proof · cited by 15
- MulEquiv.isDomainproof · cited by 8
- mul_eq_mul_left_iffstatement and proof · cited by 7
- Function.Injective.isLeftCancelMulZerostatement and proof · cited by 5
- dvd_dvd_iff_associatedstatement and proof · cited by 5
- normalize_eq_normalizestatement and proof · cited by 5
- Function.Injective.isCancelMulZeroproof · cited by 4