lean_workbook_plus_41796

Proved

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

Find $f(5)$ if $f(x)+f(\frac{1}{1-x})=x$ for all real $x \not= 0,1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_41796 (f : ℝ → ℝ) (hf : ∀ x, x ≠ 0 ∧ x ≠ 1 → f x + f ((1 / (1 - x))) = x) : f 5 = 121 / 40   :=  by sorry

Source