Theorem AlgebraicGeometry.isIso_of_isClosedImmersion_of_surjective

Modification history

2024-10-20 11:19
Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
feat(AlgebraicGeometry): affine morphisms are separated (#17962)
Added AlgebraicGeometry.isIso_of_isClosedImmersion_of_surjectiveView on Github →