Theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp

Modification history

2025-12-13 14:21

Mathlib/Geometry/RingedSpace/OpenImmersion.lean

chore: use `Category*` everywhere (#32842) …

Modified AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp View on Github →

2024-06-24 12:36

Mathlib/Geometry/RingedSpace/OpenImmersion.lean

feat(Geometry/OpenImmersion): lemmas for sheafed space/locally ringed space (#14039) …

Added AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp View on Github →