Linear_Combination_of_Derivatives
Provedcalculusderivativesproofwiki
The derivative of alphaf + betag equals alphaf' + betag'.
Preamble
import Mathlib.Analysis.Calculus.Deriv.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Calculus.Deriv.Basic theorem Linear_Combination_of_Derivatives (f g : ℝ → ℝ) (α β x : ℝ) (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) : deriv (fun t => α * f t + β * g t) x = α * deriv f x + β * deriv g x := by sorry
Source