`BookProof.ChapterTensorCompleteness.hasSum_tensorHilbertBasis` (b : HilbertBasis ι ℂ (Lp ℂ 2 μ)) (c : HilbertBasis κ ℂ (Lp ℂ 2 ν)) (F : Lp ℂ 2 (μ.prod ν)) : HasSum (fun p : ι × κ

Initializing...

`BookProof.ChapterTensorCompleteness.hasSum_tensorHilbertBasis` (b : HilbertBasis ι ℂ (Lp ℂ 2 μ)) (c : HilbertBasis κ ℂ (Lp ℂ 2 ν)) (F : Lp ℂ 2 (μ.prod ν)) : HasSum (fun p : ι × κ · Prove2Me