polynomial — Mathlib

English

If p ∈ F_q[X] is nonzero, then inftyValuationDef of its algebraMap equals exp(p.natDegree).

Русский

Если p ∈ F_q[X] не равно нулю, то в случае алгебраического отображения валюация равна exp(deg(p)).

LaTeX

$$$\text{polynomial}(p) : p \neq 0 \Rightarrow inftyValuationDef F_q (\text{algebraMap}_{F_q[X]}(p)) = \exp(\operatorname{natDegree}(p) : \mathbb{Z}).$$$

Lean4

theorem polynomial {p : Fq[X]} (hp : p ≠ 0) :
    inftyValuationDef Fq (algebraMap Fq[X] (RatFunc Fq) p) = exp (p.natDegree : ℤ) :=
  by
  have hp' : algebraMap Fq[X] (RatFunc Fq) p ≠ 0 := by simpa
  rw [inftyValuationDef, if_neg hp', RatFunc.intDegree_polynomial]

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