Theorem IsFractionRing.self_iff_nonZeroDivisors_eq_isUnit

Modification history

2025-10-25 18:20
Mathlib/RingTheory/Localization/FractionRing.lean
feat(RingTheory): Noetherian ring of fractions is semilocal (#30837) …
Added IsFractionRing.self_iff_nonZeroDivisors_eq_isUnitView on Github →