English
Let F be a field of characteristic zero and p ∈ F[X] irreducible with natDegree prime. Then natDegree of p divides the cardinality of the Galois group of its splitting field over F, i.e. p.natDegree divides Nat.card p.Gal.
Русский
Пусть F — поле нулевой характеристики и p ∈ F[X] - ирредуцируемый многочлен с простым natDegree. Тогда p.natDegree делит кардинал группы Галуа для разложения p над F, то есть p.natDegree делит Nat.card p.Gal.
LaTeX
$$$\forall F\,[Field F],\ [CharZero F], p\in F[X],\text{Irreducible } p\to p.natDegree\text{ Prime }\to p.natDegree\mid \operatorname{Nat.card}(p.Gal)$$$
Lean4
theorem prime_degree_dvd_card [CharZero F] (p_irr : Irreducible p) (p_deg : p.natDegree.Prime) :
p.natDegree ∣ Nat.card p.Gal := by
rw [Gal.card_of_separable p_irr.separable]
have hp : p.degree ≠ 0 := fun h => Nat.Prime.ne_zero p_deg (natDegree_eq_zero_iff_degree_le_zero.mpr (le_of_eq h))
let α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) (SplittingField.splits p) hp
have hα : IsIntegral F α := .of_finite F α
use Module.finrank F⟮α⟯ p.SplittingField
suffices (minpoly F α).natDegree = p.natDegree
by
letI _ : AddCommGroup F⟮α⟯ := Ring.toAddCommGroup
rw [← Module.finrank_mul_finrank F F⟮α⟯ p.SplittingField, IntermediateField.adjoin.finrank hα, this]
suffices minpoly F α ∣ p by
have key := (minpoly.irreducible hα).dvd_symm p_irr this
apply le_antisymm
· exact natDegree_le_of_dvd this p_irr.ne_zero
· exact natDegree_le_of_dvd key (minpoly.ne_zero hα)
apply minpoly.dvd F α
rw [aeval_def, map_rootOfSplits _ (SplittingField.splits p) hp]
