`BookProof.ChapterA.realCommutes_smul` {M : System ℂ V} {S : V →L[ℝ] V} (hS : RealCommutes M S) (r : ℝ) : RealCommutes M (r • S)

Initializing...

`BookProof.ChapterA.realCommutes_smul` {M : System ℂ V} {S : V →L[ℝ] V} (hS : RealCommutes M S) (r : ℝ) : RealCommutes M (r • S) · Prove2Me