`BookProof.BookBrstYangMills.AfieldPoly_apply` (μ : Fin 4) (a : Fin N) (p : FieldPoly N) : AfieldPoly μ a p = X (μ, a) * p

Initializing...

`BookProof.BookBrstYangMills.AfieldPoly_apply` (μ : Fin 4) (a : Fin N) (p : FieldPoly N) : AfieldPoly μ a p = X (μ, a) * p · Prove2Me