feat(field_theory/polynomial_galois_group): Restriction is surjective (#5961)
feat(field_theory/polynomial_galois_group): Restriction is surjective (#5961)

Proves surjectivity of `restrict` and `restrict_dvd`.



Co-authored-by: tb65536 <25c750517795e47f172dc8c552ed72c7de260bd4@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib