Commit 2021-08-27 17:22 2eaec057

feat(ring_theory): define integrally closed domains (#8893) In this follow-up to #8882, we define the notion of an integrally closed domain R, which contains all integral elements of Frac(R). We show the equivalence to is_integral_closure R R K for a field of fractions K. We provide instances for is_dedekind_domains, unique_fractorization_monoids, and to the integers of a valuation. In particular, the rational root theorem provides a proof that ℤ is integrally closed.