`BookProof.ChapterSolidHarmonic.laplacian_const_mul` {f : E → ℝ} {x : E} (c : ℝ) (hf : ContDiffAt ℝ 2 f x) : (Δ fun y => c * f y) x = c * (Δ f) x

Initializing...

`BookProof.ChapterSolidHarmonic.laplacian_const_mul` {f : E → ℝ} {x : E} (c : ℝ) (hf : ContDiffAt ℝ 2 f x) : (Δ fun y => c * f y) x = c * (Δ f) x · Prove2Me