`BookProof.ChapterBesselHarmonic.hasDerivAt_quot` {R : ℝ → ℝ} {l : ℕ} {s : ℝ} (hs : s ≠ 0) (hR : DifferentiableAt ℝ R s) : HasDerivAt (fun t => R t / t ^ l) (deriv R s / s ^ l

Initializing...

`BookProof.ChapterBesselHarmonic.hasDerivAt_quot` {R : ℝ → ℝ} {l : ℕ} {s : ℝ} (hs : s ≠ 0) (hR : DifferentiableAt ℝ R s) : HasDerivAt (fun t => R t / t ^ l) (deriv R s / s ^ l - (l · Prove2Me