lean_workbook_plus_13094

Proved

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

Find all functions $f:\mathbb{R}\to\mathbb{R}$ such that $(x+y)(f(x)-f(y))=f(x^2)-f(y^2)$ for all $x,y\in\mathbb{R}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13094 (f : ℝ → ℝ):(∀ x y, (x + y) * (f x - f y) = f (x ^ 2) - f (y ^ 2)) ↔ ∃ a b:ℝ, ∀ x, f x = a * x + b   :=  by sorry

Source