Theorems · Theorem · group theory
IsUnit.mul_left_eq_zero
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {a b : M₀}, IsUnit b → (a * b = 0 ↔ a = 0)- Cited by
- 10 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
- Assumes
- MonoidWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Unitsproof · cited by 2,804
- Units.valproof · cited by 1,966
- IsUnitstatement and proof · cited by 1,602
- MonoidWithZerostatement and proof · cited by 456
- Units.mul_left_eq_zeroproof · cited by 2
Cited by10
Results whose statement or proof uses this declaration.
- IsUnit.mem_nonZeroDivisorsproof · cited by 8
- PowerSeries.IsWeierstrassFactorizationAt.map_ne_zero_of_ne_topproof · cited by 3
- Submonoid.LocalizationMap.nonZeroDivisors_le_comapproof · cited by 2
- Submonoid.LocalizationMap.isCancelMulZeroproof · cited by 2
- IsUnit.isNilpotent_mul_unit_of_commute_iffproof · cited by 2
- Polynomial.degree_mul_C_of_isUnitproof · cited by 1
- IsLocalization.eq_zero_of_fst_eq_zeroproof · cited by 1
- Submonoid.LocalizationMap.noZeroDivisorsproof · cited by 1
- Submonoid.LocalizationMap.uniqueFactorizationMonoidproof · cited by 1
- Ideal.le_ker_atPrime_of_forall_exists_eq_mulproof · cited by 1