lean_workbook_plus_14763

Proved

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

For a certain function $f(x)$ , $f(x+y) = f(xy)-f(x)+f(-y)$ for all reals $x$ and $y$ . Given that $f(-1) = 5$ , find $f(2022)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14763 (f : ℝ → ℝ) (hf : ∀ x y, f (x + y) = f (x*y) - f x + f (-y)) : f (-1) = 5 → f 2022 = 5   :=  by sorry

Source