lean_workbook_plus_16728

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 $f(x^2-y^2)=(x-y)(f(x)+f(y))$ holds for all real values of $x$ and $y$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source