lean_workbook_plus_69983

Proved

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

Find all functions $f: \mathbb{R} \to \mathbb{R}$ such that: \n $f(x)y+1=f(xy)+y$ \n \n For all $x,y \in \mathbb{R}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_69983 (f : ℝ → ℝ): (∀ x y, f x * y + 1 = f (x * y) + y) ↔ ∃ k:ℝ, ∀ x, f x = k * x + 1   :=  by sorry

Source