Commit 2025-01-20 16:09 80485942

View on Github →

feat(AlgebraicGeometry): Formally unramified morphisms (#20603)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean

modified theorem AlgebraicGeometry.affineAnd_isLocal

added theorem AlgebraicGeometry.affineAnd_isLocal_of_propertyIsLocal

Modified Mathlib/AlgebraicGeometry/Morphisms/Finite.lean

Created Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean

added theorem AlgebraicGeometry.FormallyUnramified.of_comp

Modified Mathlib/AlgebraicGeometry/Morphisms/Integral.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean

added theorem AlgebraicGeometry.isOpenImmersion_SpecMap_iff_of_surjective