Theorems · Definition · number theory

RatFunc.uniformizingPolynomial

{K : Type u_1} →
  {Γ : Type u_2} →
    [inst : Field K] →
      [inst_1 : LinearOrderedCommGroupWithZero Γ] →
        {v : Valuation (RatFunc K) Γ} → [v.IsNontrivial] → [Valuation.IsTrivialOn K v] → v RatFunc.X ≤ 1 → Polynomial K

A uniformizing element for the valuation v, as a polynomial in K[X].

Defined in

Mathlib.NumberTheory.RatFunc.Ostrowski

Cited by

7 results in Mathlib

Foundations

Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderedCommGroupWithZeroValuation.IsNontrivialValuation.IsTrivialOn