Commit 2026-10-28 01:55 55911a1a
View on Github →refactor(Analysis/Normed): generalize scalar distance and diameter lemmas (#44829)
Generalize scalar distance and diameter lemmas to NormedRing, and drop the nonzero assumption from infDist_smul₀.