Theorem IsDiscreteValuationRing.exists_lift_of_le_one

Modification history

2026-06-08 09:51
Mathlib/RingTheory/Valuation/Discrete/Basic.lean
feat(DedekindDomain/AdicValuation): `intValuation` on uniformizers is `exp (-1)` (#37501) …
Modified IsDiscreteValuationRing.exists_lift_of_le_oneView on Github →
2025-07-26 15:56
Mathlib/RingTheory/Valuation/Discrete/Basic.lean
feat(RingTheory/Valuation/Discrete/Basic): relate DVRs and discrete valuations (#26623) …
Added IsDiscreteValuationRing.exists_lift_of_le_oneView on Github →