Def AlgebraicGeometry.Spec.toLocallyRingedSpace

Modification history

2024-04-30 23:37

Mathlib/AlgebraicGeometry/Spec.lean

perf(AlgebraicGeometry.Spec): add explicit universe annotations (#12557) …

Modified AlgebraicGeometry.Spec.toLocallyRingedSpace View on Github →

2023-06-14 02:02

Mathlib/AlgebraicGeometry/Spec.lean

feat: port AlgebraicGeometry.Spec (#4599)

Added AlgebraicGeometry.Spec.toLocallyRingedSpace View on Github →