`BookProof.ChapterSolidHarmonic.hasFDerivAt_radialFactor` (e : E) (l μ : ℕ) (x : E) : HasFDerivAt (radialFactor e l μ) (∑ m ∈ Finset.range ((l - μ) / 2 + 1), ((derivative^[μ] (lege

Initializing...

`BookProof.ChapterSolidHarmonic.hasFDerivAt_radialFactor` (e : E) (l μ : ℕ) (x : E) : HasFDerivAt (radialFactor e l μ) (∑ m ∈ Finset.range ((l - μ) / 2 + 1), ((derivative^[μ] (lege · Prove2Me