`BookProof.BookBrstYangMills.bookOmega_eq_brstCharge` : bookOmega G = Complex.I • brstCharge G.f (gaussGen G) chiOp betaOp

Initializing...

`BookProof.BookBrstYangMills.bookOmega_eq_brstCharge` : bookOmega G = Complex.I • brstCharge G.f (gaussGen G) chiOp betaOp · Prove2Me