lean_workbook_plus_28668

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that if $p(x)=a_0+a_1x+\ldots+a_nx^n$ and $q(x)=b_0+b_1x+\ldots+b_mx^m$ , then $(p+q)'(x) = p'(x) + q'(x)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_28668 (p q : Polynomial ℝ) (x : ℝ) :
  (p + q).derivative.eval x = p.derivative.eval x + q.derivative.eval x   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph