Commit 2024-10-20 11:19 1ae9a84c

View on Github →

feat(AlgebraicGeometry): affine morphisms are separated (#17962)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

added theorem AlgebraicGeometry.isIso_of_isClosedImmersion_of_surjective

Modified Mathlib/AlgebraicGeometry/Morphisms/Separated.lean

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean

added theorem AlgebraicGeometry.diagonal_Spec_map