`BookProof.ChapterA.realCommutes_add` {M : System ℂ V} {S T : V →L[ℝ] V} (hS : RealCommutes M S) (hT : RealCommutes M T) : RealCommutes M (S + T)

Initializing...

`BookProof.ChapterA.realCommutes_add` {M : System ℂ V} {S T : V →L[ℝ] V} (hS : RealCommutes M S) (hT : RealCommutes M T) : RealCommutes M (S + T) · Prove2Me