lean_workbook_plus_5193

Proved

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

Find all functions $f: R\rightarrow R$ such that: $f(x+y)+f(xy)=f(x^2)+f(y^2)$ for all $x,y$ are reals

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source