∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {ι : Type u_1} [inst_1 : Fintype ι] (f : ι → Type u_2)
  [inst_2 : (i : ι) → NormedAddCommGroup (f i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (f i)] (x y z : PiLp 2 f),
  ∑ i, inner 𝕜 (x.ofLp i + y.ofLp i) (z.ofLp i) =
    ∑ i, inner 𝕜 (x.ofLp i) (z.ofLp i) + ∑ i, inner 𝕜 (y.ofLp i) (z.ofLp i)