Theorem IsDiscreteValuationRing.mker_valuation_eq_isUnitSubmonoid

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

2026-04-14 10:54

Mathlib/RingTheory/Valuation/Discrete/Basic.lean

feat(RingTheory): Order of vanishing in a discrete valuation ring (#29550) …

Added IsDiscreteValuationRing.mker_valuation_eq_isUnitSubmonoid View on Github →