Prove2Me

lean_workbook_plus_420

Proved

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

Illustrate the solution using the quadratic equation (x−x1)(x−x2)≡x2−Sx+P=0(x-x_1)(x-x_2)\equiv x^2-Sx+P=0 where S=x1+x2S=x_1+x_2 and P=x1x2P=x_1x_2.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_420 (x x1 x2 S P : ℂ) (hx : x ≠ x1 ∧ x ≠ x2) (hS : S = x1 + x2) (hP : P = x1 * x2) : (x - x1) * (x - x2) = x^2 - S * x + P   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph