`BookProof.HermiteStrichartzQG.oscillator_eigenfunction` (n : ℕ) (x : ℝ) : -(deriv (deriv (hermiteFun n)) x) + x ^ 2 / 4 * hermiteFun n x = oscillatorSymbol n * hermiteFun n x

Initializing...

`BookProof.HermiteStrichartzQG.oscillator_eigenfunction` (n : ℕ) (x : ℝ) : -(deriv (deriv (hermiteFun n)) x) + x ^ 2 / 4 * hermiteFun n x = oscillatorSymbol n * hermiteFun n x · Prove2Me