Sum_Rule_for_Derivatives
Proveddifferential-calculusproofwikisum-rule-for-derivatives
Let f and g be real functions differentiable at a point x. Then (f + g)'(x) = f'(x) + g'(x).
Preamble
import Mathlib.Analysis.Calculus.Deriv.Add
Formal statement
theorem Sum_Rule_for_Derivatives {f g : ℝ → ℝ} {x : ℝ} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) : deriv (f + g) x = deriv f x + deriv g x := by sorrySource