`BookProof.BookBrstYangMills.sum_smul_der_apply` {n : ℕ} (k : Fin n → ℂ) (D : Fin n → Derivation ℂ (FieldPoly N) (FieldPoly N)) (p : FieldPoly N) : (∑ h, k h • D h) p = ∑ h, k h •

Initializing...

`BookProof.BookBrstYangMills.sum_smul_der_apply` {n : ℕ} (k : Fin n → ℂ) (D : Fin n → Derivation ℂ (FieldPoly N) (FieldPoly N)) (p : FieldPoly N) : (∑ h, k h • D h) p = ∑ h, k h • · Prove2Me