structure DiscreteValuation (F : Type u_1) [Field F] : Type u_1

A discrete valuation on a field $F$, i.e. a surjective homomorphism $v : F^\times \to \mathbb{Z}$ satisfying $v(x+y) \geq \min(v(x), v(y))$ (Definition 23.4). Packaged as a Mathlib Valuation valued in $\mathbb{Z}_\infty$ together with a rank-one discreteness hypothesis.

• val : Valuation F (WithZero (Multiplicative ℤ))
• val : Valuation F (WithZero (Multiplicative ℤ))
• val : Valuation F (WithZero (Multiplicative ℤ))
• discrete : self.val.IsRankOneDiscrete

def DiscreteValuation.valuationSubring {F : Type u_1} [Field F] (v : DiscreteValuation F) : ValuationSubring F

The valuation subring $R = \{x \in F : v(x) \geq 0\}$ of a discrete valuation.

def DiscreteValuation.valuationRing {F : Type u_1} [Field F] (v : DiscreteValuation F) : Subring F

The underlying subring of $F$ associated to a discrete valuation.

noncomputable def DiscreteValuation.maximalIdeal {F : Type u_1} [Field F] (v : DiscreteValuation F) : Ideal ↥v.valuationSubring

The unique maximal ideal $\mathfrak{m} = \{x \in R : v(x) \geq 1\}$ of the valuation ring.

def DiscreteValuation.IsUniformizerOf {F : Type u_1} [Field F] (v : DiscreteValuation F) (u : F) : Prop

An element $u \in F$ is a uniformizer for $v$ when $v(u) = 1$.

theorem DiscreteValuation.isPrincipalIdealRing {F : Type u_1} [Field F] (v : DiscreteValuation F) : IsPrincipalIdealRing ↥v.valuationSubring

The valuation ring of a discrete valuation is a principal ideal domain (Definition 23.4).