Theorems · Theorem · group theory
NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
∀ {M₀ : Type u_2} {inst : Mul M₀} {inst_1 : Zero M₀} [self : NoZeroDivisors M₀] {a b : M₀}, a * b = 0 → a = 0 ∨ b = 0For all a and b of M₀, a * b = 0 implies a = 0 or b = 0.
- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- NoZeroDivisors
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NoZeroDivisorsstatement and proof · cited by 545
Cited by14
Results whose statement or proof uses this declaration.
- mul_ne_zeroproof · cited by 178
- mul_eq_zeroproof · cited by 94
- Function.Injective.noZeroDivisorsproof · cited by 8
- eq_zero_of_ne_zero_of_mul_left_eq_zeroproof · cited by 7
- eq_zero_of_ne_zero_of_mul_right_eq_zeroproof · cited by 7
- Orientation.eq_zero_or_eq_zero_of_kahler_eq_zeroproof · cited by 2
- IsRegular.of_ne_zero'proof · cited by 2
- eq_zero_of_mul_self_eq_zeroproof · cited by 2
- Ideal.Quotient.isDomain_iff_primeproof · cited by 1
- AlgHom.eq_piEvalAlgHomproof · cited by 1
- irreducible_iff_prime_of_existsUnique_irreducible_factorsproof · cited by 1
- CharP.char_is_prime_of_two_leproof · cited by 1