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_sourceView on Github →