Def TopologicalSpace.IrreducibleCloseds.orderIsoOfIsOpenEmbedding

Modification history

2026-04-28 05:54

Mathlib/Topology/Sets/Closeds.lean

feat(AlgebraicGeometry): The codimension of a point of a scheme is equal to the krull dimension of the stalk (#26735) …

Added TopologicalSpace.IrreducibleCloseds.orderIsoOfIsOpenEmbedding View on Github →