`BookProof.ChapterAbelianDiagonalCountable.commutes_diagOp_iff` (T : Ell2C →L[ℂ] Ell2C) : (∀ d : EllInf, T.comp (diagOp d) = (diagOp d).comp T) ↔ ∃ d : EllInf, T = diagOp d

Initializing...

`BookProof.ChapterAbelianDiagonalCountable.commutes_diagOp_iff` (T : Ell2C →L[ℂ] Ell2C) : (∀ d : EllInf, T.comp (diagOp d) = (diagOp d).comp T) ↔ ∃ d : EllInf, T = diagOp d · Prove2Me