inftyValuation_of_nonzero — Mathlib

English

If p is a nonzero polynomial in F_q[X], the valuation of its image is exp(degree(p)).

Русский

Если p не равен нулю и является многочленом, валюация изображения равна exp(natDegree(p)).

LaTeX

$$$\text{if } p \neq 0,\ inftyValuationDef_{F_q}(p) = \exp(\operatorname{natDegree}(p))$$$

Lean4

@[simp]
theorem inftyValuation_of_nonzero {x : RatFunc Fq} (hx : x ≠ 0) : inftyValuationDef Fq x = exp x.intDegree := by
  rw [inftyValuationDef, if_neg hx]

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