Def smoothSheafCommRing

Modification history

2026-03-06 08:34

Mathlib/Geometry/Manifold/Sheaf/Smooth.lean

refactor(CategoryTheory/Sites): redefine the category of sheaves using `ObjectProperty.FullSubcategory` (#36081) …

Modified smoothSheafCommRing View on Github →

2023-10-09 13:35

Mathlib/Geometry/Manifold/Sheaf/Smooth.lean

feat: structure sheaf of a manifold (#7332) …

Added smoothSheafCommRing View on Github →