Commit 2025-10-25 22:36 b26242b1
View on Github →feat(AlgebraicGeometry/Morphisms/Flat): add a simple lemma (#30237) This PR introduces the following simple lemma:
AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine: A morphism between affine schemes is flat and surjective if and only if the corresponding map on global sections is faithfully flat.