mathlib3

6fcb704b - chore(field_theory/polynomial_galois_group): golf `gal_action_hom` (#15919)

chore(field_theory/polynomial_galois_group): golf `gal_action_hom` (#15919) We already have a more general version of this definition, we may as well implement the specialization in terms of it.