Theorems · Theorem · commutative algebra
nonZeroDivisors.ne_zero
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {x : M₀} [Nontrivial M₀], x ∈ nonZeroDivisors M₀ → x ≠ 0- Cited by
- 22 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Quot.sound
- Assumes
- MonoidWithZeroNontrivial
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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 and proof · cited by 895
- MonoidWithZerostatement and proof · cited by 456
- zero_notMem_nonZeroDivisorsproof · cited by 6
Cited by22
Results whose statement or proof uses this declaration.
- mem_nonZeroDivisors_iff_ne_zeroproof · cited by 38
- nonZeroDivisors.coe_ne_zeroproof · cited by 17
- IsField.localization_map_bijectiveproof · cited by 3
- IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisorsproof · cited by 3
- RatFunc.liftOn_mkstatement · cited by 2
- Submodule.isInternal_prime_power_torsionproof · cited by 2
- Polynomial.IsPrimitive.mul_map_mem_lifts_iffproof · cited by 2
- RatFunc.map_apply_div_ne_zeroproof · cited by 2
- ValuationRing.iff_isInteger_or_isIntegerproof · cited by 2
- IsDiscreteValuationRing.exists_lift_of_le_oneproof · cited by 2
- IsFractionRing.isInvariant_of_isIntegralproof · cited by 2
- RatFunc.liftOn'_divproof · cited by 1