Theorems · Theorem · number theory

RatFunc.valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one

∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [inst_2 : v.IsNontrivial] [inst_3 : Valuation.IsTrivialOn K v] (hle : v RatFunc.X ≤ 1)
  {p : Polynomial K},
  p ≠ 0 →
    v ((algebraMap (Polynomial K) (RatFunc K)) p) =
      v
        (↑(RatFunc.uniformizingPolynomial hle) ^
          (Associates.mk (RatFunc.valuationIdeal hle).asIdeal).count (Associates.mk (Ideal.span {p})).factors)

Defined in

Mathlib.NumberTheory.RatFunc.Ostrowski

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderedCommGroupWithZeroValuation.IsNontrivialValuation.IsTrivialOn