Integral closure of ideals

Stream: maths

[Walter Moreira]

I see that Mathlib has the notion of integral closure of rings (docs#integralClosure). Does Mathlib has the similar notion of integral closure of ideals, as in https://en.wikipedia.org/wiki/Integral_closure_of_an_ideal?

[Johan Commelin]

I'm not aware of it

[Riccardo Brasca]

I am almost sure we don't have it.

[Walter Moreira]

Thank you for the confirmation, folks. Might take a stab at introducing a definition. We are also hoping with @Joe Stubbs to work towards introducing the tight closure of an ideal.