Commit 2023-06-24 15:03 4646748a

View on Github →

feat: port FieldTheory.AbelRuffini (#5424)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/AbelRuffini.lean

added inductive IsSolvableByRad

added theorem gal_C_isSolvable

added theorem gal_X_isSolvable

added theorem gal_X_pow_isSolvable

added theorem gal_X_pow_sub_C_isSolvable

added theorem gal_X_pow_sub_C_isSolvable_aux

added theorem gal_X_pow_sub_one_isSolvable

added theorem gal_X_sub_C_isSolvable

added theorem gal_isSolvable_of_splits

added theorem gal_isSolvable_tower

added theorem gal_mul_isSolvable

added theorem gal_one_isSolvable

added theorem gal_prod_isSolvable

added theorem gal_zero_isSolvable

added def solvableByRad.P

added theorem solvableByRad.induction1

added theorem solvableByRad.induction2

added theorem solvableByRad.induction3

added theorem solvableByRad.induction

added theorem solvableByRad.isIntegral

added theorem solvableByRad.isSolvable'

added theorem solvableByRad.isSolvable

added def solvableByRad

added theorem splits_X_pow_sub_one_of_X_pow_sub_C