Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-22 12:15 418dc044

View on Github →

feat(100-theorems-list/16_abel_ruffini): The Abel-Ruffini Theorem (#7562) It's done!

Estimated changes

Created archive/100-theorems-list/16_abel_ruffini.lean

added theorem abel_ruffini.coeff_five_Phi

added theorem abel_ruffini.coeff_zero_Phi

added theorem abel_ruffini.complex_roots_Phi

added theorem abel_ruffini.degree_Phi

added theorem abel_ruffini.exists_not_solvable_by_rad

added theorem abel_ruffini.gal_Phi

added theorem abel_ruffini.irreducible_Phi

added theorem abel_ruffini.leading_coeff_Phi

added theorem abel_ruffini.map_Phi

added theorem abel_ruffini.monic_Phi

added theorem abel_ruffini.nat_degree_Phi

added theorem abel_ruffini.not_solvable_by_rad'

added theorem abel_ruffini.not_solvable_by_rad

added theorem abel_ruffini.real_roots_Phi_ge

added theorem abel_ruffini.real_roots_Phi_ge_aux

added theorem abel_ruffini.real_roots_Phi_le

Modified docs/100.yaml

Modified src/field_theory/separable.lean

added theorem polynomial.card_root_set_eq_nat_degree