mathlib

cbdf7b56 - feat(ring_theory/*): generalise `minpoly.dvd` to integrally closed rings (#18021)

feat(ring_theory/*): generalise `minpoly.dvd` to integrally closed rings (#18021) This PR generalizes some of the theory of `minpoly` to the setting of integrally closed rings. The main results proven here are: - `minpoly.is_integrally_closed_eq_field_fractions` and variants of it - `minpoly.is_integrally_closed_dvd` - `monic.dvd_of_fraction_map_dvd_fraction_map` In a following PR, I will remove instances of `gcd_domain_dvd` (and the other results this PR generalises) from other files, and replace the file `minpoly.gcd_domain` by `minpoly.is_integrally_closed` Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>