Theorem AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine

Modification history

2025-10-25 22:36
Mathlib/AlgebraicGeometry/Morphisms/Flat.lean
feat(AlgebraicGeometry/Morphisms/Flat): add a simple lemma (#30237) …
Added AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffineView on Github →