English
A general induction principle on solvable-by-radical elements: P is preserved under algebraic operations and radical powers, starting from the base field.
Русский
Общая индуктивная принципия на элементах, разрешимых радикалами: P сохраняется под алгебраическими операциями и радикальными степенями, начиная с базового поля.
LaTeX
$$$$\text{SolvableByRad.induction: } P(α) \text{ for all } α \in solvableByRad F E,$$ with closure under +, -, ×, ^{-1}, and α^n.$$
Lean4
/-- An auxiliary induction lemma, which is generalized by `solvableByRad.isSolvable`. -/
theorem induction1 {α β : solvableByRad F E} (hβ : β ∈ F⟮α⟯) (hα : P α) : P β :=
induction2 (adjoin.mono F _ _ (ge_of_eq (Set.pair_eq_singleton α)) hβ) hα hα
