Commit 2021-05-10 07:36 38bf2abd

View on Github →

feat(field_theory/abel_ruffini): Version of solvable_by_rad.is_solvable (#7509) This is a version of solvable_by_rad.is_solvable, which will be the final step of the abel-ruffini theorem.

Estimated changes

Modified src/field_theory/abel_ruffini.lean

added theorem solvable_by_rad.is_solvable'

Modified src/field_theory/minpoly.lean

added theorem minpoly.unique''