mathlib3

88525a98 - feat(ring_theory/ideal): generalize from `integral_closure` to `is_integral_closure` (#8944)

feat(ring_theory/ideal): generalize from `integral_closure` to `is_integral_closure` (#8944) This PR restates a couple of lemmas about ideals the integral closure to use an instance of `is_integral_closure` instead. The originals are still available, but their proofs are now oneliners shelling out to `is_integral_closure`.