Theorems · Theorem · group theory
IsLeftCancelMulZero.mul_left_cancel_of_ne_zero
∀ {M₀ : Type u} {inst : Mul M₀} {inst_1 : Zero M₀} [self : IsLeftCancelMulZero M₀] {a : M₀}, a ≠ 0 → IsLeftRegular aMultiplication by a nonzero element is left cancellative.
- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- IsLeftCancelMulZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- IsLeftRegularstatement · cited by 97
- IsLeftCancelMulZerostatement and proof · cited by 48
Cited by4
Results whose statement or proof uses this declaration.
- mul_left_cancel₀proof · cited by 47
- IsMulTorsionFree.pow_right_injective₀proof · cited by 2
- Polynomial.isLeftCancelMulZero_iffproof · cited by 1
- Ideal.relNorm_eq_pow_of_isPrime_isGaloisproof · cited by 1