mathlib

8bdf5e9b - refactor(field_theory/polynomial_galois_group): remove `open_locale classical` (#19184)

refactor(field_theory/polynomial_galois_group): remove `open_locale classical` (#19184) This doesn't actually generalize any lemmas, but it reduces the chance of lemmas added in future being less general. The `restrict_dvd_def` lemma is new, and deals with substituting an arbitray `decidable_eq` instance.