English
For every natural number n, the Galois group of the polynomial X^n − 1 over F is solvable.
Русский
Для любого натурального числа n группа Галуа полинома X^n − 1 над F разрешима.
LaTeX
$$$$\forall n \in \mathbb{N},\ IsSolvable\big((X^n - 1 : F[X]).Gal\big)$$$$
Lean4
theorem gal_X_pow_sub_one_isSolvable (n : ℕ) : IsSolvable (X ^ n - 1 : F[X]).Gal :=
by
by_cases hn : n = 0
· rw [hn, pow_zero, sub_self]
exact gal_zero_isSolvable
have hn' : 0 < n := pos_iff_ne_zero.mpr hn
have hn'' : (X ^ n - 1 : F[X]) ≠ 0 := X_pow_sub_C_ne_zero hn' 1
apply isSolvable_of_comm
intro σ τ
ext a ha
simp only [mem_rootSet_of_ne hn'', map_sub, aeval_X_pow, aeval_one, sub_eq_zero] at ha
have key : ∀ σ : (X ^ n - 1 : F[X]).Gal, ∃ m : ℕ, σ a = a ^ m :=
by
intro σ
lift n to ℕ+ using hn'
exact map_rootsOfUnity_eq_pow_self σ.toAlgHom (rootsOfUnity.mkOfPowEq a ha)
obtain ⟨c, hc⟩ := key σ
obtain ⟨d, hd⟩ := key τ
rw [σ.mul_apply, τ.mul_apply, hc, map_pow, hd, map_pow, hc, ← pow_mul, pow_mul']
