`BookProof.HarmonicOscillator.hasDerivAt_polyGaussC` (p : Polynomial ℝ) (x : ℝ) : HasDerivAt (polyGaussC p) ((((derivative p - C (1 / 2 : ℝ) * (X * p)).eval x * gaussH x : ℝ) : ℂ))

Initializing...

`BookProof.HarmonicOscillator.hasDerivAt_polyGaussC` (p : Polynomial ℝ) (x : ℝ) : HasDerivAt (polyGaussC p) ((((derivative p - C (1 / 2 : ℝ) * (X * p)).eval x * gaussH x : ℝ) : ℂ)) · Prove2Me