valuation_le_one_of_valuation_X_le_one

English

The valuation on RatFunc(K) is given by the valuation attached to the X-ideal: v(x) = valuation_{idealX(K)}(x).

Русский

Оценка на RatFunc(K) задаётся оценкой, связанной с идеалом X: v(x) = valuation_{idealX(K)}(x).

LaTeX

$$$v(x) = \operatorname{valuation}_{(\operatorname{idealX}(K))}(x)$$$

Lean4

/-- If a valuation `v` is trivial on constants and `v RatFunc.X ≤ 1` then for every polynomial `p`,
`v p ≤ 1`. -/
theorem valuation_le_one_of_valuation_X_le_one (hle : v RatFunc.X ≤ 1) (p : K[X]) : v p ≤ 1 :=
  by
  rw [as_sum_range p, RatFunc.coePolynomial, map_sum]
  apply map_sum_le v
  intro i
  by_cases h0 : p.coeff i = 0
  · simp_all
  · rw [← RatFunc.coePolynomial]
    simp_all [valuation_monomial_eq_valuation_X_pow, pow_le_one']

Похожие утверждения