`BookProof.BookBrstYangMills.bosOpN_sum3` (T : Fin 4 → Fin N → Fin N → Module.End ℂ (FieldPoly N)) : bosOpN (∑ μ, ∑ a, ∑ b, T μ a b) = ∑ μ, ∑ a, ∑ b, bosOpN (T μ a b)

Initializing...

`BookProof.BookBrstYangMills.bosOpN_sum3` (T : Fin 4 → Fin N → Fin N → Module.End ℂ (FieldPoly N)) : bosOpN (∑ μ, ∑ a, ∑ b, T μ a b) = ∑ μ, ∑ a, ∑ b, bosOpN (T μ a b) · Prove2Me