lean_workbook_plus_63979

Proved

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

Find all function $f:\mathbb{R} \to \mathbb{R}$ such that, \n\n

f(x+y)=x+f(y), ~~~\forall x,y \in \mathbb{R}.

\n\n

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source