`BookProof.BookBrstYangMills.bosOpN_rsmul` (r : ℝ) (T : Module.End ℂ (FieldPoly N)) : bosOpN (r • T) = r • bosOpN T

Initializing...

`BookProof.BookBrstYangMills.bosOpN_rsmul` (r : ℝ) (T : Module.End ℂ (FieldPoly N)) : bosOpN (r • T) = r • bosOpN T · Prove2Me