Commit 2025-05-23 11:00 46a4e374
View on Github →chore(RingTheory/IntegralClosure): remove duplicate (#25120) The duplicate lemma was introduced earlier today in #25066. I have renamed it to the old name and removed the old one (because it needs more import and arguably lives in the wrong file)