English
An auxiliary induction lemma used to build solvability results by induction on powers.
Русский
Вспомогательная лемма индукции для построения результатов разрешимости по степеням.
LaTeX
$$$$\text{Induction3: auxiliary step for powers, as used in solvableByRad.isSolvable.}$$$$
Lean4
/-- An auxiliary induction lemma, which is generalized by `solvableByRad.isSolvable`. -/
theorem induction3 {α : solvableByRad F E} {n : ℕ} (hn : n ≠ 0) (hα : P (α ^ n)) : P α :=
by
let p := minpoly F (α ^ n)
have hp : p.comp (X ^ n) ≠ 0 := by
intro h
rcases comp_eq_zero_iff.mp h with h' | h'
· exact minpoly.ne_zero (isIntegral (α ^ n)) h'
· exact hn (by rw [← @natDegree_C F, ← h'.2, natDegree_X_pow])
apply gal_isSolvable_of_splits
·
exact
⟨splits_of_splits_of_dvd _ hp (SplittingField.splits (p.comp (X ^ n)))
(minpoly.dvd F α (by rw [aeval_comp, aeval_X_pow, minpoly.aeval]))⟩
· refine gal_isSolvable_tower p (p.comp (X ^ n)) ?_ hα ?_
· exact Gal.splits_in_splittingField_of_comp _ _ (by rwa [natDegree_X_pow])
· obtain ⟨s, hs⟩ := (splits_iff_exists_multiset _).1 (SplittingField.splits p)
rw [map_comp, Polynomial.map_pow, map_X, hs, mul_comp, C_comp]
apply gal_mul_isSolvable (gal_C_isSolvable _)
rw [multiset_prod_comp]
apply gal_prod_isSolvable
intro q hq
rw [Multiset.mem_map] at hq
obtain ⟨q, hq, rfl⟩ := hq
rw [Multiset.mem_map] at hq
obtain ⟨q, _, rfl⟩ := hq
rw [sub_comp, X_comp, C_comp]
exact gal_X_pow_sub_C_isSolvable n q
