mathlib3

b1c56b1b - feat(field_theory.minimal_polynomial): add results for GCD domains (#5336)

feat(field_theory.minimal_polynomial): add results for GCD domains (#5336) I have added `gcd_domain_dvd`: for GCD domains, the minimal polynomial divides any primitive polynomial that has the integral element as root. For `gcd_domain_eq_field_fractions` and `gcd_domain_dvd` I have also added explicit versions for `ℤ`. Unfortunately, it seems impossible (to me at least) to apply the general lemmas and I had to redo the proofs, see [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Minimal.20polynomial.20over.20.E2.84.9A.20vs.20over.20.E2.84.A4) for more details. (The basic reason seems to be that it's hard to convince lean that `is_scalar_tower ℤ ℚ α` holds using the localization map).