Theorems · Definition · commutative algebra
nonZeroDivisors
(M₀ : Type u_1) → [inst : MonoidWithZero M₀] → Submonoid M₀
The submonoid of non-zero-divisors of a MonoidWithZero M₀.
- Cited by
- 895 results in Mathlib
- Foundations
- Depth 15 from the axioms, rests on 86 definitions · uses propext, Quot.sound
- Assumes
- MonoidWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Submonoidstatement · cited by 3,086
- MonoidWithZerostatement and proof · cited by 456
- nonZeroDivisorsLeftproof · cited by 26
- nonZeroDivisorsRightproof · cited by 26
Cited by994
Results whose statement or proof uses this declaration.
- IsFractionRingproof · cited by 738
- FractionRingproof · cited by 200
- ClassGroupproof · cited by 50
- FractionRing.liftAlgebrastatement · cited by 43
- mem_nonZeroDivisors_iff_ne_zerostatement · cited by 38
- mem_nonZeroDivisors_of_ne_zerostatement · cited by 34
- Ideal.dvd_iff_leproof · cited by 33
- FractionalIdeal.dualstatement and proof · cited by 33
- DivisibleHullproof · cited by 30
- FractionalIdeal.extendedHomstatement · cited by 26
- NumberField.integralBasisproof · cited by 25
- FractionalIdeal.countstatement and proof · cited by 25
Showing the 200 most cited of 994.