Structures · Algebra
NoZeroDivisors
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
- Shape
- One type argument · adds eq_zero_or_eq_zero_of_mul_eq_zero
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances35
- NNReal
- ENNReal
- Polynomial
- Quaternion
- HahnSeries
- ENat
- EReal
- MonoidAlgebra
- AddMonoidAlgebra
- Zsqrtd
- Localization
- WittVector
- SetSemiring
- Tropical
- MvPowerSeries
- Ordinal
- Cardinal
- SymmetricAlgebra
- Associates
- FreeAlgebra
- TensorAlgebra
- MvPolynomial
- PowerSeries
- Subtype
- OrderDual
- MulOpposite
- Lex
- AddOpposite
- HasQuotient.Quotient
- WithTop
- WithBot
- Submodule
- WithZero
- Set
- Finset
How is a type an instance?
Loading the hierarchy index…
Assumed by618
- mul_ne_zero
- mul_eq_zero
- Finset.prod_ne_zero_iff
- mul_ne_zero_iff
- mem_nonZeroDivisors_iff_ne_zero
- mem_nonZeroDivisors_of_ne_zero
- FractionalIdeal.dual
- Polynomial.leadingCoeff_mul
- Polynomial.degree_mul
- Polynomial.natDegree_mul
- Ideal.primeCompl_le_nonZeroDivisors
- AlgebraicIndependent.matroid
- Function.support_mul
- NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
- Polynomial.degree_eq_zero_of_isUnit
- sq_eq_one_iff
- CharP.char_is_prime_or_zero
- Polynomial.natDegree_comp
- WeierstrassCurve.Projective.X_eq_zero_of_Z_eq_zero
- Algebra.IsAlgebraic.trans
- Polynomial.natDegree_le_of_dvd
- Polynomial.natDegree_pow
- Polynomial.isUnit_iff
- Polynomial.natDegree_C_mul
- meromorphicOrderAt_smul
- mul_self_inj_of_nonneg
- MonomialOrder.degree_mul
- Finset.prod_eq_zero_iff
- Function.Injective.noZeroDivisors
- WeakDual.gelfandTransform
- add_self_eq_zero
- MonoidWithZeroHom.one_apply_of_ne_zero
- eq_zero_of_ne_zero_of_mul_right_eq_zero
- eq_zero_of_ne_zero_of_mul_left_eq_zero
- Multiset.prod_eq_zero_iff
- MonoidWithZeroHom.one_apply_zero
- IsTranscendenceBasis.lift_cardinalMk_eq_trdeg
- cfcₙ_nonneg
- mul_self_eq_one_iff
- nonZeroDivisors_le_comap_nonZeroDivisors_of_injective
- Polynomial.coe_normUnit
- mul_self_eq_zero
- AbsoluteValue.map_sub
- zero_eq_mul
- IsAlgebraic.restrictScalars
- CharZero.eq_neg_self_iff
- Polynomial.degree_C_mul
- Polynomial.leadingCoeffHom
- map_le_nonZeroDivisors_of_injective
- mul_eq_zero_iff_right
Ancestors0
No ancestors.