`BookProof.YangMillsAbelianNoGap.gaussInt_bigP` : gaussInt (bigP vf Mf * bigP vf Mf) = (((∏ j, facS vf Mf j) * (Real.sqrt (2 * Real.pi)) ^ d : ℝ) : ℂ)

Initializing...

`BookProof.YangMillsAbelianNoGap.gaussInt_bigP` : gaussInt (bigP vf Mf * bigP vf Mf) = (((∏ j, facS vf Mf j) * (Real.sqrt (2 * Real.pi)) ^ d : ℝ) : ℂ) · Prove2Me