`BookProof.ChapterA.IsRReal.not_hasCommutingRImaginary` [Nontrivial W] {M : System ℝ W} (h : IsRReal M) : ¬ HasCommutingRImaginary M

Initializing...

`BookProof.ChapterA.IsRReal.not_hasCommutingRImaginary` [Nontrivial W] {M : System ℝ W} (h : IsRReal M) : ¬ HasCommutingRImaginary M · Prove2Me