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_domain`s, `unique_fractorization_monoid`s, and to the integers of a valuation. In particular, the rational root theorem provides a proof that `ℤ` is integrally closed.
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
