English
The map cardPowDegree defines a Euclidean function on Fq[X], i.e., Fq[X] is Euclidean with respect to degree.
Русский
Карта cardPowDegree задаёт евклидову функцию на F_q[X], то есть F_q[X] является евклидовым по степени.
LaTeX
$$$\mathrm{IsEuclidean}\left(\operatorname{cardPowDegree} : \operatorname{AbsoluteValue} F_q[X] \mathbb{Z}\right)$$$
Lean4
theorem cardPowDegree_isEuclidean : IsEuclidean (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
{
map_lt_map_iff' := fun {p q} => by
classical
change cardPowDegree p < cardPowDegree q ↔ degree p < degree q
simp only [cardPowDegree_apply]
split_ifs with hp hq hq
· simp only [hp, hq, lt_self_iff_false]
· simp only [hp, hq, degree_zero, Ne, bot_lt_iff_ne_bot, degree_eq_bot, pow_pos, not_false_iff]
· simp only [hq, degree_zero, not_lt_bot, (pow_pos _).not_gt]
· rw [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt, pow_lt_pow_iff_right₀]
exact mod_cast @Fintype.one_lt_card Fq _ _ }
