Commit 2023-06-24 19:08 21fb5acc

View on Github →

feat: port Archive.Wiedijk100Theorems.AbelRuffini (#5457)

Estimated changes

Modified Archive.lean

Created Archive/Wiedijk100Theorems/AbelRuffini.lean

added theorem AbelRuffini.coeff_five_Phi

added theorem AbelRuffini.coeff_zero_Phi

added theorem AbelRuffini.complex_roots_Phi

added theorem AbelRuffini.degree_Phi

added theorem AbelRuffini.exists_not_solvable_by_rad

added theorem AbelRuffini.gal_Phi

added theorem AbelRuffini.irreducible_Phi

added theorem AbelRuffini.leadingCoeff_Phi

added theorem AbelRuffini.map_Phi

added theorem AbelRuffini.monic_Phi

added theorem AbelRuffini.natDegree_Phi

added theorem AbelRuffini.not_solvable_by_rad'

added theorem AbelRuffini.not_solvable_by_rad

added theorem AbelRuffini.real_roots_Phi_ge

added theorem AbelRuffini.real_roots_Phi_ge_aux

added theorem AbelRuffini.real_roots_Phi_le