Commit 2020-12-14 16:39 b1c56b1b

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 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).