lean_workbook_plus_77012

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 for all $x,y\in\mathbb{R},$ $f\left(x+xf(y)\right)=x+yf\left(f(x)\right).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_77012 (f : ℝ → ℝ): (∀ x y, f (x + x * f y) = x + y * f (f x)) ↔ ∀ x, f x = x   :=  by sorry

Source