English
For all n and x ∈ F, the Galois group of X^n − C x is solvable, extending the previous results.
Русский
Для всех n и x ∈ F, Галуа-Галуа группы X^n − C x разрешимы, подтверждая предыдущие результаты.
LaTeX
$$$$\forall n \in \mathbb{N},\ x \in F,\ IsSolvable\big((X^n - C x).Gal\big)$$$$
Lean4
/-- **Abel-Ruffini Theorem** (one direction): An irreducible polynomial with an
`IsSolvableByRad` root has solvable Galois group -/
theorem isSolvable' {α : E} {q : F[X]} (q_irred : Irreducible q) (q_aeval : aeval α q = 0) (hα : IsSolvableByRad F α) :
IsSolvable q.Gal :=
by
have : _root_.IsSolvable (q * C q.leadingCoeff⁻¹).Gal :=
by
rw [minpoly.eq_of_irreducible q_irred q_aeval, ←
show minpoly F (⟨α, hα⟩ : solvableByRad F E) = minpoly F α from
(minpoly.algebraMap_eq (RingHom.injective _) _).symm]
exact isSolvable ⟨α, hα⟩
refine solvable_of_surjective (Gal.restrictDvd_surjective ⟨C q.leadingCoeff⁻¹, rfl⟩ ?_)
rw [mul_ne_zero_iff, Ne, Ne, C_eq_zero, inv_eq_zero]
exact ⟨q_irred.ne_zero, leadingCoeff_ne_zero.mpr q_irred.ne_zero⟩
