Mathlib Changelog
v4
Changelog
About
Github
Theorem
AlgebraicGeometry.IsOpenImmersion.of_openCover_source
Modification history
2025-10-06 20:40
Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean
feat(AlgebraicGeometry): quasi-affine schemes (#30256)
Added
AlgebraicGeometry.IsOpenImmersion.of_openCover_source
View on Github →