Theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'

Modification history

2024-10-16 11:05

Mathlib/Geometry/RingedSpace/OpenImmersion.lean

refactor(AlgebraicGeometry): Make `Scheme.Hom` a structure. (#15093) …

Modified AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'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.LocallyRingedSpace.IsOpenImmersion.app_inv_app'View on Github →