Theorems · Theorem · number theory

RatFunc.valuation_isEquiv_infty_or_adic

• 1000+ list: Ostrowski's theorem

∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [v.IsRankOneDiscrete] [Valuation.IsTrivialOn K v] [inst_4 : DecidableEq (RatFunc K)],
  Xor (v.IsEquiv (RatFunc.inftyValuation K))
    (∃! u, v.IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) u))

Ostrowski's Theorem for K(X) with K any field: A discrete valuation of rank 1 that is trivial on K is equivalent either to the valuation at infinity or to the p-adic valuation for a unique maximal ideal p of K[X].

Defined in

Mathlib.NumberTheory.RatFunc.Ostrowski

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderedCommGroupWithZeroValuation.IsRankOneDiscreteValuation.IsTrivialOnDecidableEq