Commit 2026-06-22 07:32 95284251

View on Github →

feat(Topology/SmallInductiveDimension): fix small style issues (#40878) We make some arguments implicit, change Type to Type*, and fix some capitalization.

Estimated changes

Modified Mathlib/Topology/SmallInductiveDimension.lean

deleted theorem HasSmallInductiveDimensionLT_one_iff

deleted theorem HasSmallInductiveDimensionLT_zero_iff

added theorem hasSmallInductiveDimensionLT_one_iff

added theorem hasSmallInductiveDimensionLT_zero_iff