Theorems · Theorem · group theory
mul_ne_zero
∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [NoZeroDivisors M₀] {a b : M₀}, a ≠ 0 → b ≠ 0 → a * b ≠ 0- Defined in
- Mathlib.Algebra.GroupWithZero.Basic
- Cited by
- 178 results in Mathlib
- Foundations
- Depth 7 from the axioms, rests on 23 definitions · uses no axioms
- Assumes
- MulZeroNoZeroDivisors
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.
- NoZeroDivisorsstatement and proof · cited by 545
- NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zeroproof · cited by 14
Cited by178
Results whose statement or proof uses this declaration.
- Real.log_mulproof · cited by 52
- Polynomial.leadingCoeff_mulproof · cited by 32
- meromorphicOrderAt_eq_int_iffproof · cited by 31
- div_ne_zeroproof · cited by 29
- Polynomial.degree_mulproof · cited by 25
- Polynomial.natDegree_mulproof · cited by 23
- Real.Gamma_pos_of_posproof · cited by 17
- Complex.mul_cpow_ofReal_nonnegproof · cited by 12
- UniqueFactorizationMonoid.normalizedFactors_mulproof · cited by 11
- Polynomial.associated_content_mulproof · cited by 6
- Real.circleAverage_zeroproof · cited by 6
- Complex.canonicalFactor_ne_zeroproof · cited by 6