mathlib3

63a17823 - feat(field_theory/polynomial_galois_group): More flexible version of gal_action_hom_bijective_of_prime_degree (#7508)

feat(field_theory/polynomial_galois_group): More flexible version of gal_action_hom_bijective_of_prime_degree (#7508) Since the number of non-real roots is even, we can make a more flexible version of `gal_action_hom_bijective_of_prime_degree`. This flexibility will be helpful when working with a specific polynomial.