Theorem IsDiscreteValuationRing.associated_of_valuation_eq

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