`BookProof.HarmonicOscillator.deriv_const_mul_fun` (c : ℂ) {f : ℝ → ℂ} (hf : ∀ x, DifferentiableAt ℝ f x) : deriv (fun x => c * f x) = fun x => c * deriv f x

Initializing...

`BookProof.HarmonicOscillator.deriv_const_mul_fun` (c : ℂ) {f : ℝ → ℂ} (hf : ∀ x, DifferentiableAt ℝ f x) : deriv (fun x => c * f x) = fun x => c * deriv f x · Prove2Me