Theorems · Inductive type · group theory
IsRightCancelMulZero
(M₀ : Type u) → [Mul M₀] → [Zero M₀] → Prop
A mixin for right cancellative multiplication by nonzero elements.
- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Cited by
- 33 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 by37
Results whose statement or proof uses this declaration.
- mul_left_inj'statement and proof · cited by 35
- mul_left_injective₀statement and proof · cited by 22
- mul_right_cancel₀statement and proof · cited by 22
- mul_eq_mul_right_iffstatement and proof · cited by 12
- MulEquiv.isDomainproof · cited by 8
- mul_eq_right₀statement and proof · cited by 7
- eq_zero_of_mul_eq_self_leftstatement and proof · cited by 5
- Function.Injective.isCancelMulZeroproof · cited by 4
- eq_zero_or_one_of_sq_eq_selfstatement and proof · cited by 4
- Function.Injective.isRightCancelMulZerostatement and proof · cited by 4
- right_eq_mul₀statement and proof · cited by 3
- isCancelMulZero_iff_noZeroDivisorsproof · cited by 2