Theorem AlgebraicGeometry.Surjective.sigmaDesc_of_union_range_eq_univ

Modification history

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