lean_workbook_plus_7839

Proved

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

For two functions $f(x)=ax^2+bx+c$ and $g(x)=a^{'}x^2+b^{'}x+c^{'}$ , $f(x)=g(x)$ holds for all $x \in R$ if and only if $a=a^{'}$ , $b=b^{'}$ and $c=c^{'}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7839  (a b c a' b' c' : ℝ)
  (f g : ℝ → ℝ)
  (h₀ : ∀ x, f x = a * x ^ 2 + b * x + c)
  (h₁ : ∀ x, g x = a' * x ^ 2 + b' * x + c')
  (h₂ : ∀ x, f x = g x) :
  a = a' ∧ b = b' ∧ c = c'   :=  by sorry

Source

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

View graph