(c : ι → ℝ) (f : lpFiniteModes ι) (i : ι) : (((lpDiag c f : lpFiniteModes ι) : lp (fun _ : ι => ℂ) 2) : ι → ℂ) i = (c i : ℂ) * ((f : lp (fun _ : ι => ℂ) 2) : ι → ℂ) i

Initializing...

(c : ι → ℝ) (f : lpFiniteModes ι) (i : ι) : (((lpDiag c f : lpFiniteModes ι) : lp (fun _ : ι => ℂ) 2) : ι → ℂ) i = (c i : ℂ) * ((f : lp (fun _ : ι => ℂ) 2) : ι → ℂ) i · Prove2Me