mathlib

f151da2a - feat(field_theory/polynomial_galois_group): Restriction from splitting field of composition (#6148)

feat(field_theory/polynomial_galois_group): Restriction from splitting field of composition (#6148) Defines the surjective restriction map from the splitting field of a composition Co-authored-by: tb65536 <tb65536@users.noreply.github.com>