Theorems · Theorem · group theory
mul_eq_mul_left_iff
∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [IsLeftCancelMulZero M₀] {a b c : M₀}, a * b = a * c ↔ b = c ∨ a = 0- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MulZeroClass.zero_mulproof · cited by 1,625
- MulZeroClassstatement and proof · cited by 232
- IsLeftCancelMulZerostatement and proof · cited by 48
Cited by7
Results whose statement or proof uses this declaration.
- Rat.add_num_den'proof · cited by 2
- WittVector.select_add_select_notproof · cited by 2
- MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq_innerproof · cited by 1
- IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_oneproof · cited by 1
- mul_right_eq_self₀proof · cited by 1
- NNReal.mul_eq_mul_leftproof · cited by 0
- Rat.mul_num_den'proof · cited by 0