Theorem IsDiscreteValuationRing.RingEquivClass.isDiscreteValuationRing

Modification history

2024-12-20 22:56
Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
feat(DiscreteValuationRing/Basic): a ring equivalent to a DVR is a DVR (#20073) …
Added IsDiscreteValuationRing.RingEquivClass.isDiscreteValuationRingView on Github →