Theorem AlgebraicGeometry.coheight_eq_of_isOpenImmersion

Modification history

2026-04-28 05:54
Mathlib/AlgebraicGeometry/Properties.lean
feat(AlgebraicGeometry): The codimension of a point of a scheme is equal to the krull dimension of the stalk (#26735) …
Added AlgebraicGeometry.coheight_eq_of_isOpenImmersionView on Github →