Commit 2026-10-02 10:03 16b46e22

feat(Analysis/Normed/Order): generalize distance lemmas to solid norms (#44072) Generalize the distance lemmas for finite products of reals to normed lattice-ordered additive groups with a solid norm. Add the instances needed so that the generalized lemmas apply directly to ℝ, finite products ι → ℝ, and EuclideanSpace ℝ.