`BookProof.ChapterAbelianDiagonalCountable.diagOp_smul` (c : ℂ) (d : EllInf) : diagOp (c • d) = c • diagOp d

Initializing...

`BookProof.ChapterAbelianDiagonalCountable.diagOp_smul` (c : ℂ) (d : EllInf) : diagOp (c • d) = c • diagOp d · Prove2Me