Commit 2020-06-24 09:30 194edc12

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.