Theorems · Theorem · group theory
mul_eq_mul_right_iff
∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [IsRightCancelMulZero M₀] {a b c : M₀}, a * c = b * c ↔ a = b ∨ c = 0- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Cited by
- 12 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.mul_zeroproof · cited by 2,091
- MulZeroClassstatement and proof · cited by 232
- IsRightCancelMulZerostatement and proof · cited by 33
Cited by12
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.addHaarScalarFactor_eq_mulproof · cited by 6
- Complex.Gamma_mul_Gamma_one_subproof · cited by 3
- MeasureTheory.Measure.haarScalarFactor_eq_mulproof · cited by 3
- sum_range_powproof · cited by 2
- mul_left_eq_self₀proof · cited by 2
- bernoulli'_eq_zero_of_oddproof · cited by 2
- Nat.bell_eq_sum_eraseproof · cited by 1
- Finpartition.card_filter_equitabilise_smallproof · cited by 1
- EuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_distproof · cited by 1
- Behrend.map_eq_iffproof · cited by 1
- divisor_closure_eq_closureproof · cited by 0
- Quaternion.sq_eq_normSqproof · cited by 0