Theorem AlgebraicGeometry.isOpenImmersion_SpecMap_iff_of_surjective

Modification history

2025-01-20 16:09
Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean
feat(AlgebraicGeometry): Formally unramified morphisms (#20603)
Added AlgebraicGeometry.isOpenImmersion_SpecMap_iff_of_surjectiveView on Github →