Commit 2024-06-23 14:59 5c12fd76

View on Github →

feat(Geometry/RingedSpace/OpenImmersion): make IsOpenImmersion instance (#14050)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/Cover/Open.lean

Modified Mathlib/AlgebraicGeometry/Restrict.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

modified theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict

modified theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict

modified theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso

Modified Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean