Def AlgebraicGeometry.sigmaSpec

Modification history

2025-07-23 11:19
Mathlib/AlgebraicGeometry/Limits.lean
feat: `Spec(R)` notation for `Spec (CommRingCat.of R)` (#27031) …
Modified AlgebraicGeometry.sigmaSpecView on Github →
2024-08-02 19:53
Mathlib/AlgebraicGeometry/Limits.lean
feat(AlgebraicGeometry/Limits): Spec preserves finite coproducts (#14428)
Added AlgebraicGeometry.sigmaSpecView on Github →