mathlib3

01088844 - feat(ring_theory/integral_closure): A subalgebra is contained in the integral closure iff it is integral (#10874)