Theorems · Theorem · commutative algebra
mem_nonZeroDivisors_of_ne_zero
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {x : M₀} [NoZeroDivisors M₀], x ≠ 0 → x ∈ nonZeroDivisors M₀- Cited by
- 34 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
- Assumes
- MonoidWithZeroNoZeroDivisors
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Submonoidstatement · cited by 3,086
- nonZeroDivisorsstatement · cited by 895
- NoZeroDivisorsstatement and proof · cited by 545
- MonoidWithZerostatement and proof · cited by 456
- eq_zero_of_ne_zero_of_mul_left_eq_zeroproof · cited by 7
- eq_zero_of_ne_zero_of_mul_right_eq_zeroproof · cited by 7
Cited by35
Results whose statement or proof uses this declaration.
- mem_nonZeroDivisors_iff_ne_zeroproof · cited by 38
- le_nonZeroDivisors_of_noZeroDivisorsproof · cited by 5
- IsAlgebraic.of_mulproof · cited by 4
- IsAlgebraic.restrictScalars_of_isIntegralproof · cited by 4
- Polynomial.derivative_rootMultiplicity_of_rootproof · cited by 3
- isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injectiveproof · cited by 2
- Matrix.rank_mul_eq_right_of_det_ne_zeroproof · cited by 2
- Matrix.nondegenerate_of_det_ne_zeroproof · cited by 2
- OreLocalization.inv_defstatement · cited by 2
- Algebra.IsAlgebraic.exists_smul_eq_mulproof · cited by 2
- isAddTorsion_iff_isTorsion_intproof · cited by 2
- Algebra.IsAlgebraic.injective_tower_topproof · cited by 2