mathlib

c271266b - feat(ring_theory): the integral closure `C` of `A` is Noetherian over `A` (#15381)

feat(ring_theory): the integral closure `C` of `A` is Noetherian over `A` (#15381) where `A` is an integrally closed Noetherian domain and `C` is the closure in a finite separable extension `L` of `Frac(A)` I was going to use this in https://github.com/leanprover-community/mathlib/pull/15315 but it turns out we don't assume separability there. Since it might still be useful elsewhere, I turned it into a new PR. The proof was already in mathlib, as part of showing that the integral closure of a Dedekind domain is Noetherian, so I could just split off the part that dealt with Noetherianness. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>