Def ChartedSpace.restrictLocallyRingedSpaceIso

Modification history

2026-04-01 16:05

Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean

feat(Geometry/Manifold): a smooth map induces a morphism of locally ringed spaces (#35661)

Added ChartedSpace.restrictLocallyRingedSpaceIso View on Github →