feat(ring_theory): a typeclass `is_integral_closure` (#8882)
The typeclass `is_integral_closure A R B` states `A` is the integral closure of `R` in `B`, i.e. that an element of `B` is integral over `R` iff it is an element of (the image of) `A`.
We also show that any integral extension of `R` contained in `B` is contained in `A`, and the integral closure is unique up to isomorphism.
This was suggested in the review of #8701, in order to define a characteristic predicate for rings of integers.
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
