`BookProof.BookBrstYangMills.gaussDer_apply` (c : Fin N) (p : FieldPoly N) : gaussDer G c p = ∑ i : Fin 4 × Fin N, gaussVec G c i * pderiv i p

Initializing...

`BookProof.BookBrstYangMills.gaussDer_apply` (c : Fin N) (p : FieldPoly N) : gaussDer G c p = ∑ i : Fin 4 × Fin N, gaussVec G c i * pderiv i p · Prove2Me