`BookProof.ChapterBesselHarmonic.reduced_from_radial` {R : ℝ → ℝ} {l : ℕ} {p r : ℝ} (hr : r ≠ 0) (hR : DifferentiableAt ℝ R r) (hR' : DifferentiableAt ℝ (deriv R) r) (hRev : ∀ᶠ s i

Initializing...

`BookProof.ChapterBesselHarmonic.reduced_from_radial` {R : ℝ → ℝ} {l : ℕ} {p r : ℝ} (hr : r ≠ 0) (hR : DifferentiableAt ℝ R r) (hR' : DifferentiableAt ℝ (deriv R) r) (hRev : ∀ᶠ s i · Prove2Me