From 88525a98b72bbc970cd919fa18155f40bcac459b Mon Sep 17 00:00:00 2001
From: Anne Baanen <vierkantor@vierkantor.com>
Date: Thu, 2 Sep 2021 14:35:26 +0000
Subject: [PATCH] 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`.