Commit 2025-11-20 20:48 30c4d389

feat: ofLp and toLp of a sum (#31353) Introduce an AddEquiv version of WithLp.equiv and use it to prove that (∑ i ∈ s, f i).ofLp = ∑ i ∈ s, (f i).ofLp and toLp p (∑ i ∈ s, f i) = ∑ i ∈ s, toLp p (f i).