Def AlgebraicGeometry.Proj.basicOpenIsoAway

Modification history

2026-09-04 11:59

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean

chore(CategoryTheory): use the new `↧` notation in concrete categories (#41811) …

Modified AlgebraicGeometry.Proj.basicOpenIsoAway View on Github →

2024-11-17 17:51

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean

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

Added AlgebraicGeometry.Proj.basicOpenIsoAway View on Github →