`BookProof.ChapterSolidHarmonicTools.laplacian_cylTerm` (e : E) (he : ‖e‖ = 1) (j m : ℕ) (x : E) : (Δ fun y : E => (⟪e, y⟫_ℝ) ^ j * (‖y‖ ^ 2) ^ m) x = (j : ℝ) * ((j : ℝ)

Initializing...

`BookProof.ChapterSolidHarmonicTools.laplacian_cylTerm` (e : E) (he : ‖e‖ = 1) (j m : ℕ) (x : E) : (Δ fun y : E => (⟪e, y⟫_ℝ) ^ j * (‖y‖ ^ 2) ^ m) x = (j : ℝ) * ((j : ℝ) - 1)... · Prove2Me