Commit 2026-04-21 17:27 faab47f0

View on Github →

feat(topology): Small inductive dimension (#37619) Adds a type class for small inductive dimension. See also https://github.com/leanprover-community/mathlib4/pull/37444. AI disclosure: Claude code assisted in preparing this PR.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/SmallInductiveDimension.lean

added theorem HasSmallInductiveDimensionLT_one_iff

added theorem HasSmallInductiveDimensionLT_zero_iff