Commit 2021-03-19 09:01 86e1b175

View on Github →

feat(field_theory/abel_ruffini): solvable by radicals implies solvable Galois group (#6631) Proves the theoretical part of insolvability of the quintic. We still need to exhibit a specific polynomial with non-solvable Galois group

Estimated changes

Created src/field_theory/abel_ruffini.lean

added theorem gal_C_is_solvable

added theorem gal_X_is_solvable

added theorem gal_X_pow_is_solvable

added theorem gal_X_pow_sub_C_is_solvable

added theorem gal_X_pow_sub_C_is_solvable_aux

added theorem gal_X_pow_sub_one_is_solvable

added theorem gal_X_sub_C_is_solvable

added theorem gal_is_solvable_of_splits

added theorem gal_is_solvable_tower

added theorem gal_mul_is_solvable

added theorem gal_one_is_solvable

added theorem gal_prod_is_solvable

added theorem gal_zero_is_solvable

added inductive is_solvable_by_rad

added def solvable_by_rad.P

added theorem solvable_by_rad.induction1

added theorem solvable_by_rad.induction2

added theorem solvable_by_rad.induction3

added theorem solvable_by_rad.induction

added theorem solvable_by_rad.is_integral

added theorem solvable_by_rad.is_solvable

added def solvable_by_rad

added theorem splits_X_pow_sub_one_of_X_pow_sub_C