Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-17 23:27 cbdf7b56

View on Github →

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

Estimated changes

modified theorem minpoly.gcd_domain_dvd
deleted theorem minpoly.gcd_domain_unique
added theorem minpoly.ker_eval