Prove2Me

lean_workbook_plus_21880

Proved

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

Find all functions f:R→Rf : \mathbb{R} \to \mathbb{R} such that f(x−y)+f(y−z)−f(z−x)=f(x+y+z)f(x-y)+f(y-z)-f(z-x)=f(x+y+z), where xy+yz+zx=0xy+yz+zx=0.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_21880 (f : ℝ → ℝ):(∀ x y z:ℝ, (x*y+y*z+z*x=0 → f (x-y) + f (y-z) - f (z-x) = f (x+y+z))) ↔ ∃ c:ℝ, ∀ x:ℝ, f x = c   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph