lean_workbook_plus_30241

Proved

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

Write $P(x)=x(x-1)(x-2)Q(x)+ax^2+bx+c$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_30241 (a b c : ℝ) (Q : ℝ → ℝ) (P : ℝ → ℝ) (h₁ : P = fun x => x * (x - 1) * (x - 2) * Q x + a * x ^ 2 + b * x + c) : ∃ a b c : ℝ, ∀ x : ℝ, P x = x * (x - 1) * (x - 2) * Q x + a * x ^ 2 + b * x + c   :=  by sorry

Source

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

View graph