`BookProof.ChapterLinftyMultiplication.multOp_one` : multOp (fun _ : α => (1 : ℂ)) memLp_top_one = ContinuousLinearMap.id ℂ (Lp ℂ 2 μ)

Initializing...

`BookProof.ChapterLinftyMultiplication.multOp_one` : multOp (fun _ : α => (1 : ℂ)) memLp_top_one = ContinuousLinearMap.id ℂ (Lp ℂ 2 μ) · Prove2Me