Def AlgebraicGeometry.Proj.basicOpenToSpec

Modification history

2025-07-23 11:19

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean

feat: `Spec(R)` notation for `Spec (CommRingCat.of R)` (#27031) …

Modified AlgebraicGeometry.Proj.basicOpenToSpec View on Github →

2024-11-17 17:51

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean

feat(AlgebraicGeometry): basic API for `Proj` (#19152)

Added AlgebraicGeometry.Proj.basicOpenToSpec View on Github →