lean_workbook_plus_62529

Proved

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

Find all functions $f: R\rightarrow R$ ,that satisfy to the following condition: For all $x,y\in R$ : $(x+y)(f(x)-f(y))=(x-y)(f(x)+f(y))$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source