English
Let Fq be a finite field. There is a canonical absolute-value on Fq[X], cardPowDegree, which assigns 0 to 0 and q^{deg p} to nonzero polynomials p, where q = |Fq|.
Русский
Пусть Fq — конечное поле. Существуют каноническая окрестная функция-абсолютное значение cardPowDegree на Fq[X], которая отправляет 0 в 0 и q^{deg p} в любые ненулевые полиномы p, где q = |Fq|.
LaTeX
$$$ cardPowDegree : \\text{AbsoluteValue } Fq[X] \\mathbb{Z} $ сards 0 для 0 и $q^{\\deg p}$ для ненулевого p, где q = |Fq|.$$
Lean4
/-- `cardPowDegree` is the absolute value on `𝔽_q[t]` sending `f` to `q ^ degree f`.
`cardPowDegree 0` is defined to be `0`. -/
noncomputable def cardPowDegree : AbsoluteValue Fq[X] ℤ :=
have card_pos : 0 < Fintype.card Fq := Fintype.card_pos_iff.mpr inferInstance
have pow_pos : ∀ n, 0 < (Fintype.card Fq : ℤ) ^ n := fun n => pow_pos (Int.natCast_pos.mpr card_pos) n
letI := Classical.decEq Fq
{ toFun := fun p => if p = 0 then 0 else (Fintype.card Fq : ℤ) ^ p.natDegree
nonneg' := fun p => by
split_ifs
· rfl
exact pow_nonneg (Int.ofNat_zero_le _) _
eq_zero' := fun p =>
ite_eq_left_iff.trans
⟨fun h => by
contrapose! h
exact ⟨h, (pow_pos _).ne'⟩, absurd⟩
add_le' := fun p q => by
by_cases hp : p = 0; · simp [hp]
by_cases hq : q = 0; · simp [hq]
by_cases hpq : p + q = 0
· simp only [hpq, hp, hq, if_true, if_false]
exact add_nonneg (pow_pos _).le (pow_pos _).le
simp only [hpq, hp, hq, if_false]
exact le_trans (pow_right_mono₀ (by cutsat) (Polynomial.natDegree_add_le _ _)) (by grind)
map_mul' := fun p q => by
by_cases hp : p = 0; · simp [hp]
by_cases hq : q = 0; · simp [hq]
have hpq : p * q ≠ 0 := mul_ne_zero hp hq
simp only [hpq, hp, hq, if_false, Polynomial.natDegree_mul hp hq, pow_add] }
