Mathlib Changelog
v4
Changelog
About
Github
Def
AlgebraicGeometry.LocallyRingedSpace.toRingedSpace
Modification history
2025-02-25 18:02
Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
chore(AlgebraicGeometry): clean up `erw` and porting notes (#22272) …
Deleted
AlgebraicGeometry.LocallyRingedSpace.toRingedSpace
View on Github →
2023-06-02 15:12
Mathlib/AlgebraicGeometry/LocallyRingedSpace.lean
feat: port AlgebraicGeometry.LocallyRingedSpace (#4589)
Added
AlgebraicGeometry.LocallyRingedSpace.toRingedSpace
View on Github →