lean_workbook_plus_67171

Proved

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

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

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67171 (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