Commit 2026-03-20 17:27 e5a473e9

View on Github →

chore(FieldTheory/AbelRuffini): simpler definition of solvableByRad (#35908) We redefine solvableByRad F E as the smallest intermediate field closed under n-th roots. This makes the predicate IsSolvableByRad redundant, and so we deprecate it. We also private/remove various auxiliary results, and change the statement of the Abel-Ruffini theorem to be about an element of the field, rather than the subtype.

Estimated changes

Modified Archive/Wiedijk100Theorems/AbelRuffini.lean

modified theorem AbelRuffini.exists_not_solvable_by_rad

modified theorem AbelRuffini.not_solvable_by_rad'

Modified Mathlib/Algebra/Field/Subfield/Basic.lean

modified theorem Subfield.mem_sInf

Modified Mathlib/FieldTheory/AbelRuffini.lean

added theorem isAlgebraic_solvableByRad

added theorem isIntegral_of_mem_solvableByRad

added theorem isSolvable_gal_minpoly

added theorem isSolvable_gal_of_irreducible

deleted def solvableByRad.P

deleted theorem solvableByRad.induction1

deleted theorem solvableByRad.induction2

deleted theorem solvableByRad.induction3

deleted theorem solvableByRad.induction

deleted theorem solvableByRad.isIntegral

deleted theorem solvableByRad.isSolvable'

deleted theorem solvableByRad.isSolvable

added theorem solvableByRad.rad_mem

modified def solvableByRad

added theorem solvableByRad_le

added theorem solvableByRad_le_algClosure

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean

modified theorem IntermediateField.coe_sInf

added theorem IntermediateField.mem_sInf