mathlib

194edc12 - feat(ring_theory/localization): integral closure in field extension (#3096)

feat(ring_theory/localization): integral closure in field extension (#3096) Let `A` be an integral domain with field of fractions `K` and `L` a finite extension of `K`. This PR shows the integral closure of `A` in `L` has fraction field `L`. If those definitions existed, the corollary is that the ring of integers of a number field is a number ring. For this, we need two constructions on polynomials: * If `p` is a nonzero polynomial, `integral_normalization p` is a monic polynomial with roots `z * a` for `z` a root of `p` and `a` the leading coefficient of `p` * If `f` is the localization map from `A` to `K` and `p` has coefficients in `K`, then `f.integer_normalization p` is a polynomial with coefficients in `A` (think: `∀ i, is_integer (f.integer_normalization p).coeff i`) with the same roots as `p`.