English
Let K/F be a field extension with K finite. Then K is the splitting field over F of the polynomial X^{|K|} - X in F[X].
Русский
Пусть K/F — конечное расширение полей. Тогда K является полем разложения над F для многочлена X^{|K|} - X в F[X].
LaTeX
$$IsSplittingField F K (X^{|K|} - X)$$
Lean4
instance isSplittingField_sub (K F : Type*) [Field K] [Fintype K] [Field F] [Algebra F K] :
IsSplittingField F K (X ^ Fintype.card K - X)
where
splits' :=
by
have h : (X ^ Fintype.card K - X : K[X]).natDegree = Fintype.card K :=
FiniteField.X_pow_card_sub_X_natDegree_eq K Fintype.one_lt_card
rw [← splits_id_iff_splits, splits_iff_card_roots, Polynomial.map_sub, Polynomial.map_pow, map_X, h,
FiniteField.roots_X_pow_card_sub_X K, ← Finset.card_def, Finset.card_univ]
adjoin_rootSet' := by
classical
trans Algebra.adjoin F ((roots (X ^ Fintype.card K - X : K[X])).toFinset : Set K)
· simp only [rootSet, aroots, Polynomial.map_pow, map_X, Polynomial.map_sub]
· rw [FiniteField.roots_X_pow_card_sub_X, val_toFinset, coe_univ, Algebra.adjoin_univ]
