English
The set of elements of E that are solvable by radicals over F forms an intermediate field of E over F.
Русский
Множество элементов E, разрешимых радикалами над F, образует промежуточное поле E над F.
LaTeX
$$$$\text{solvableByRad} = \{ x \in E : x \text{ is solvable by radicals over } F \}$$$$
Lean4
/-- Inductive definition of solvable by radicals -/
inductive IsSolvableByRad : E → Prop
| base (α : F) : IsSolvableByRad (algebraMap F E α)
| add (α β : E) : IsSolvableByRad α → IsSolvableByRad β → IsSolvableByRad (α + β)
| neg (α : E) : IsSolvableByRad α → IsSolvableByRad (-α)
| mul (α β : E) : IsSolvableByRad α → IsSolvableByRad β → IsSolvableByRad (α * β)
| inv (α : E) : IsSolvableByRad α → IsSolvableByRad α⁻¹
| rad (α : E) (n : ℕ) (hn : n ≠ 0) : IsSolvableByRad (α ^ n) → IsSolvableByRad α
