lean_workbook_plus_65171

Proved

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

For the case $f(0) = 2$ , making $y=0$ : $f(x) + f(x)f(0) = f(0) + f(x) + f(0)$ __ $2f(x) = 4$ __ $f(x) = 2 (const.) (OK!)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_65171 (x : ℝ) (f : ℝ → ℝ) (hf: f 0 = 2) (h : ∀ x, f x + (f x) * (f 0) = f 0 + f x + f 0) : f x = 2   :=  by sorry

Source