Theorems · Inductive type · group theory
NoZeroDivisors
(M₀ : Type u_2) → [Mul M₀] → [Zero M₀] → Prop
Predicate typeclass for expressing that a * b = 0 implies a = 0 or b = 0
for all a and b of type M₀. It is weaker than IsCancelMulZero in general,
but equivalent to it if M₀ is a (not necessarily unital or associative) ring.
- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Cited by
- 545 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by559
Results whose statement or proof uses this declaration.
- mul_ne_zerostatement and proof · cited by 178
- mul_eq_zerostatement and proof · cited by 94
- Finset.prod_ne_zero_iffstatement and proof · cited by 45
- mul_ne_zero_iffstatement and proof · cited by 39
- mem_nonZeroDivisors_iff_ne_zerostatement and proof · cited by 38
- mem_nonZeroDivisors_of_ne_zerostatement and proof · cited by 34
- FractionalIdeal.dualstatement and proof · cited by 33
- Polynomial.leadingCoeff_mulstatement and proof · cited by 32
- Polynomial.degree_mulstatement and proof · cited by 25
- Polynomial.natDegree_mulstatement and proof · cited by 23
- Ideal.primeCompl_le_nonZeroDivisorsstatement and proof · cited by 17
- AlgebraicIndependent.matroidstatement and proof · cited by 17
Showing the 200 most cited of 559.