Def AlgebraicGeometry.pointsPi

Modification history

2025-07-23 11:19

Mathlib/AlgebraicGeometry/PointsPi.lean

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

Modified AlgebraicGeometry.pointsPi View on Github →

2025-01-30 15:54

Mathlib/AlgebraicGeometry/PointsPi.lean

feat(AlgebraicGeometry): `Π Rᵢ`-points of schemes (#20494)

Added AlgebraicGeometry.pointsPi View on Github →