Theorem IsDiscreteValuationRing.map_algebraMap_eq_valuationSubring

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.map_algebraMap_eq_valuationSubringView on Github →