Commit 2024-07-11 10:12 63c917ab

View on Github →

feat(Geometry/RingedSpace): Initial object in LocallyRingedSpace (#14549)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean

added def CategoryTheory.Limits.IsInitial.ofStrict

added def CategoryTheory.Limits.IsTerminal.ofStrict

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean

added def AlgebraicGeometry.LocallyRingedSpace.empty

added def AlgebraicGeometry.LocallyRingedSpace.emptyIsInitial

added def AlgebraicGeometry.LocallyRingedSpace.emptyTo