`BookProof.ChapterSolidHarmonicTools.laplacian_normSqPow` (m : ℕ) (x : E) : (Δ fun y : E => (‖y‖ ^ 2) ^ m) x = (4 * m * ((m : ℝ) - 1) + 2 * (Module.finrank ℝ E) * m) * (‖x‖ ^ 2) ^

Initializing...

`BookProof.ChapterSolidHarmonicTools.laplacian_normSqPow` (m : ℕ) (x : E) : (Δ fun y : E => (‖y‖ ^ 2) ^ m) x = (4 * m * ((m : ℝ) - 1) + 2 * (Module.finrank ℝ E) * m) * (‖x‖ ^ 2) ^ · Prove2Me