Theorem AlgebraicGeometry.IsOpenImmersion.of_forall_source_exists

Modification history

2025-10-06 20:40
Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean
feat(AlgebraicGeometry): quasi-affine schemes (#30256)
Added AlgebraicGeometry.IsOpenImmersion.of_forall_source_existsView on Github →