Theorem IsInducing.topologicalKrullDim_le

Modification history

2025-11-03 14:11

Mathlib/Topology/KrullDimension.lean

feat(Topology/KrullDimension): add subspace dimension inequality (#29728) …

Added IsInducing.topologicalKrullDim_le View on Github →