lean_workbook_plus_44294

Proved

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

Find all functions $f:\mathbb R\rightarrow\mathbb R$ such that for all $x,y\in\mathbb R$ ,\n\n $(x+y)(f(x)-f(y)) = (x-y)(f(x)+f(y))$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source