lean_workbook_plus_72520

Proved

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

Let $r$ be a (not necessarily real) root of $Q(x)-1=0$ . Substituting $x=r$ gives\n\n P(1)=0\nTherefore, $1$ is a root of $P$ . We have $P(1)=a+b+c\implies c=-a-b$ . This gives us:\n\n P(x)=ax^2+bx-a-b=(x-1)(ax+a+b)

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72520  (a b c : ℂ)
  (f : ℂ → ℂ)
  (h₀ : ∀ x, f x = a * x^2 + b * x + c)
  (h₁ : f 1 = 0) :
  c = -a - b   :=  by sorry

Source

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

View graph