Def IsDiscreteValuationRing.maximalIdeal

Modification history

2025-07-26 15:56

Mathlib/RingTheory/Valuation/Discrete/Basic.lean

feat(RingTheory/Valuation/Discrete/Basic): relate DVRs and discrete valuations (#26623) …

Added IsDiscreteValuationRing.maximalIdeal View on Github →