Mathlib Changelog
v4
Changelog
About
Github
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