`BookProof.BookBrstYangMills.gaussDer_bracket` (c e : Fin N) : ⁅gaussDer G c, gaussDer G e⁆ = ∑ h, ((G.f c e h : ℝ) : ℂ) • gaussDer G h

Initializing...

`BookProof.BookBrstYangMills.gaussDer_bracket` (c e : Fin N) : ⁅gaussDer G c, gaussDer G e⁆ = ∑ h, ((G.f c e h : ℝ) : ℂ) • gaussDer G h · Prove2Me