Commit 2025-12-11 10:09 fbaa01cc
View on Github →chore(RingTheory/Smooth): demote superseded instance to theorem (#32720)
Algebra.Smooth.flat_of_isNoetherianRing is now superseded by Algebra.Smooth.flat, so the former does not need to be an instance.