Def AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace

Modification history

2023-06-15 03:08

Mathlib/AlgebraicGeometry/SheafedSpace.lean

feat: relax universe constraint in `AlgebraicGeometry/SheafedSpace` and `AlgebraicGeometry/RingedSpace` (#5047)

Modified AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace View on Github →

2023-05-26 23:07

Mathlib/AlgebraicGeometry/SheafedSpace.lean

feat: port AlgebraicGeometry.SheafedSpace (#4405)

Added AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace View on Github →