Theorem Ring.isUnit_iff_ordFrac_one_of_isDiscreteValuationRing

Modification history

2026-04-14 10:54
Mathlib/RingTheory/OrderOfVanishing/Noetherian.lean
feat(RingTheory): Order of vanishing in a discrete valuation ring (#29550) …
Added Ring.isUnit_iff_ordFrac_one_of_isDiscreteValuationRingView on Github →