`BookProof.ChapterSolidHarmonic.laplacian_angular_mul_sum` {A : E → ℝ} {x e : E} (he : ‖e‖ = 1) {μ : ℕ} (n : ℕ) (h3 : Module.finrank ℝ E = 3) (hA : ContDiffAt ℝ 2 A x) (hharm : (Δ

Initializing...

`BookProof.ChapterSolidHarmonic.laplacian_angular_mul_sum` {A : E → ℝ} {x e : E} (he : ‖e‖ = 1) {μ : ℕ} (n : ℕ) (h3 : Module.finrank ℝ E = 3) (hA : ContDiffAt ℝ 2 A x) (hharm : (Δ · Prove2Me