2026-10-19 12:30
Mathlib/RingTheory/Valuation/Discrete/IsDiscreteValuationRing.lean
feat(RingTheory/Valuation/Discrete/IsDiscreteValuationSubring): equivalent discrete valuations (#43655) …
Added IsDiscreteValuationRing.maximalIdeal_valuation_isEquiv