Def AlgebraicGeometry.primeSpectrumOrderIsoSpec

Modification history

2026-09-04 11:59
Mathlib/AlgebraicGeometry/Scheme.lean
chore(CategoryTheory): use the new `↧` notation in concrete categories (#41811) …
Modified AlgebraicGeometry.primeSpectrumOrderIsoSpecView on Github →
2026-04-28 05:54
Mathlib/AlgebraicGeometry/Scheme.lean
feat(AlgebraicGeometry): The codimension of a point of a scheme is equal to the krull dimension of the stalk (#26735) …
Added AlgebraicGeometry.primeSpectrumOrderIsoSpecView on Github →