`BookProof.ChapterF2.bargmann_numberOp_re` (p : ℂ[X]) : (bargmann p (numberOp p)).re = ∑ n ∈ p.support, ((n : ℝ) * n.factorial) * Complex.normSq (p.coeff n)

Initializing...

`BookProof.ChapterF2.bargmann_numberOp_re` (p : ℂ[X]) : (bargmann p (numberOp p)).re = ∑ n ∈ p.support, ((n : ℝ) * n.factorial) * Complex.normSq (p.coeff n) · Prove2Me