Theorems · Theorem · field theory

Polynomial.valuation_le_one_of_valuation_X_le_one

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

If a valuation v is trivial on constants and v RatFunc.X ≤ 1 then for every polynomial p, v p ≤ 1.

Defined in

Mathlib.FieldTheory.RatFunc.AsPolynomial

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderedCommGroupWithZeroValuation.IsTrivialOn