English
There is an induction principle for solvable-by-radical elements: if a property P holds for the base field and is preserved under addition, negation, multiplication, inversion, and taking nth powers within the radical closure, then it holds for all solvable-by-radical elements.
Русский
Существует принцип индукции для элементов, разрешимых радикалами: если свойство P верно для базового поля и сохраняется при сложении, отрицании, умножении, взятии обратного и возведении в степень n внутри радикального замыкания, то оно верно для всех элементов, разрешимых радикалами.
LaTeX
$$$$\text{Induction: } P(\alpha) \\text{holds for all } \alpha \in \text{solvableByRad}\ F E,$$ with the usual closure properties under +, -, ×, ^{-1}, and powers.$$
Lean4
/-- The intermediate field of solvable-by-radicals elements -/
def solvableByRad : IntermediateField F E where
carrier := IsSolvableByRad F
zero_mem' := by
change IsSolvableByRad F 0
convert IsSolvableByRad.base (E := E) (0 : F); rw [RingHom.map_zero]
add_mem' := by apply IsSolvableByRad.add
one_mem' := by
change IsSolvableByRad F 1
convert IsSolvableByRad.base (E := E) (1 : F); rw [RingHom.map_one]
mul_mem' := by apply IsSolvableByRad.mul
inv_mem' := IsSolvableByRad.inv
algebraMap_mem' := IsSolvableByRad.base
