English
For every natural n and every x ∈ F, the Galois group of X^n − C x over F is solvable.
Русский
Для каждого натурального n и каждого x ∈ F, галуа-группа X^n − C x над F разрешима.
LaTeX
$$$$\forall n \in \mathbb{N},\ x \in F,\ IsSolvable\big((X^n - C x).Gal\big)$$$$
Lean4
theorem gal_X_pow_sub_C_isSolvable (n : ℕ) (x : F) : IsSolvable (X ^ n - C x).Gal :=
by
by_cases hx : x = 0
· rw [hx, C_0, sub_zero]
exact gal_X_pow_isSolvable n
apply gal_isSolvable_tower (X ^ n - 1) (X ^ n - C x)
· exact splits_X_pow_sub_one_of_X_pow_sub_C _ n hx (SplittingField.splits _)
· exact gal_X_pow_sub_one_isSolvable n
· rw [Polynomial.map_sub, Polynomial.map_pow, map_X, map_C]
apply gal_X_pow_sub_C_isSolvable_aux
have key := SplittingField.splits (X ^ n - 1 : F[X])
rwa [← splits_id_iff_splits, Polynomial.map_sub, Polynomial.map_pow, map_X, Polynomial.map_one] at key
