Module

Normalized.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Normalized

2 declarations indexed from sourceView source ↗

Module documentation

Integer-valued normalization of a discrete valuation

The maximal ideal of the actual valuation ring supplies an integer-valued discrete valuation on its fraction field. Its valuation subring is the original subring of that same field, without a Henselianity assumption.

Imports3

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Basic
Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
Mathlib.Algebra.Ring.Subring.Basic

Imported by8

theorem

exists_normalized_valuation_with_uniformizer

L24 ↗

ValuationTheory.DiscreteValuationField.DVF.exists_normalized_valuation_with_uniformizer

Documentation

Normalize a discrete valuation together with an element of value exp(-1).

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ValuationTheory.DiscreteValuationField.DVF
universe u v

Lean source · statement

theorem exists_normalized_valuation_with_uniformizer
    {K : Type u} [Field K] (base : DVF.{u, v} K) :
    ∃ w : _root_.Valuation K (WithZero (Multiplicative ℤ)),
      w.IsRankOneDiscrete ∧ w.valuationSubring = base.valuation.valuationSubring ∧
        ∃ π : K, w π = WithZero.exp (-1 : ℤ)

theorem

exists_normalized_valuation

L56 ↗

ValuationTheory.DiscreteValuationField.DVF.exists_normalized_valuation