`BookProof.ChapterFreeFieldGaussian.charFun_stdGaussian` (t : EuclideanSpace ℝ (Fin n)) : charFun (stdGaussian n) t = Complex.exp (-‖t‖ ^ 2 / 2)

Initializing...

`BookProof.ChapterFreeFieldGaussian.charFun_stdGaussian` (t : EuclideanSpace ℝ (Fin n)) : charFun (stdGaussian n) t = Complex.exp (-‖t‖ ^ 2 / 2) · Prove2Me