Commit 2024-12-20 22:56 2f2de82a
View on Github →feat(DiscreteValuationRing/Basic): a ring equivalent to a DVR is a DVR (#20073) We add the lemma saying that if a ring is isomorphic to a DVR it is itself a DVR.
feat(DiscreteValuationRing/Basic): a ring equivalent to a DVR is a DVR (#20073) We add the lemma saying that if a ring is isomorphic to a DVR it is itself a DVR.