Theorems · Theorem · commutative algebra
mem_nonZeroDivisors_iff_ne_zero
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {x : M₀} [NoZeroDivisors M₀] [Nontrivial M₀],
x ∈ nonZeroDivisors M₀ ↔ x ≠ 0- Cited by
- 38 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Submonoidstatement · cited by 3,086
- Nontrivialstatement and proof · cited by 2,416
- nonZeroDivisorsstatement · cited by 895
- NoZeroDivisorsstatement and proof · cited by 545
- MonoidWithZerostatement and proof · cited by 456
- mem_nonZeroDivisors_of_ne_zeroproof · cited by 34
- nonZeroDivisors.ne_zeroproof · cited by 22
Cited by38
Results whose statement or proof uses this declaration.
- IsIntegralClosure.isLocalizationproof · cited by 13
- FractionalIdeal.exists_eq_spanSingleton_mulproof · cited by 6
- IsFractionRing.isFractionRing_of_isDomain_of_isLocalizationproof · cited by 6
- FractionalIdeal.dual_ne_zeroproof · cited by 5
- Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_mapproof · cited by 4
- RatFunc.mk_eq_localization_mkstatement and proof · cited by 4
- Ring.ordFrac_eq_ordproof · cited by 4
- RatFunc.liftMonoidWithZeroHom_apply_divproof · cited by 4
- IsFractionRing.surjective_iff_isFieldproof · cited by 2
- RatFunc.liftOn_mkproof · cited by 2
- RatFunc.valuation_eq_LaurentSeries_valuationproof · cited by 2
- RatFunc.map_apply_div_ne_zeroproof · cited by 2