`BookProof.BookBrstYangMills.rsmul_eq_csmul` (r : ℝ) (T : Module.End ℂ (BookState N)) : r • T = ((r : ℝ) : ℂ) • T

Initializing...

`BookProof.BookBrstYangMills.rsmul_eq_csmul` (r : ℝ) (T : Module.End ℂ (BookState N)) : r • T = ((r : ℝ) : ℂ) • T · Prove2Me