Theorem AlgebraicGeometry.Flat.isQuotientMap_of_surjective

Modification history

2025-04-03 11:07
Mathlib/AlgebraicGeometry/Morphisms/Flat.lean
feat(AlgebraicGeometry): faithfully flat morphisms are topological quotient maps (#23608)
Added AlgebraicGeometry.Flat.isQuotientMap_of_surjectiveView on Github →