English
Over a finite field K of q elements, the roots of X^q − X in K are exactly all elements of K.
Русский
Для конечного поля K с q элементами корни X^q − X совпадают с множеством всех элементов K.
LaTeX
$$$\\operatorname{roots}\\left(X^q - X : K[X]\\right) = \\operatorname{Finset.univ} \\text{ (in } K) \\quad\\text{with } q=|K|$$$
Lean4
theorem roots_X_pow_card_sub_X : roots (X ^ q - X : K[X]) = Finset.univ.val := by
classical
have aux : (X ^ q - X : K[X]) ≠ 0 := X_pow_card_sub_X_ne_zero K Fintype.one_lt_card
have : (roots (X ^ q - X : K[X])).toFinset = Finset.univ :=
by
rw [eq_univ_iff_forall]
intro x
rw [Multiset.mem_toFinset, mem_roots aux, IsRoot.def, eval_sub, eval_pow, eval_X, sub_eq_zero, pow_card]
rw [← this, Multiset.toFinset_val, eq_comm, Multiset.dedup_eq_self]
apply nodup_roots
rw [separable_def]
convert isCoprime_one_right.neg_right (R := K[X]) using 1
rw [derivative_sub, derivative_X, derivative_X_pow, Nat.cast_card_eq_zero K, C_0, zero_mul, zero_sub]
