Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-05 12:11 915bff47

View on Github →

feat(field_theory/polynomial_galois_group): Restriction is surjective (#5961) Proves surjectivity of restrict and restrict_dvd.

Estimated changes