Theorem Algebra.Smooth.flat_of_isNoetherianRing

Modification history

2025-12-11 10:09
Mathlib/RingTheory/Smooth/Flat.lean
chore(RingTheory/Smooth): demote superseded `instance` to `theorem` (#32720) …
Added Algebra.Smooth.flat_of_isNoetherianRingView on Github →