lean_workbook_plus_15851

Proved

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

Given $f(f(x))=x$ for all $x$ and $(x+f(y))(f(x)+y)=xf(x)+yf(y)+2yf(x)$ , find $f(x)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_15851 (f : ℝ → ℝ) (hf1 : ∀ x, f (f x) = x) (hf2 : ∀ x y, (x + f y) * (f x + y) = x * f x + y * f y + 2 * y * f x) : ∃ h :ℝ, ∀ x, f x = h * x   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph