lean_workbook_plus_43083

Proved

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

Determine all functions $f : \mathbb{N} \to \mathbb{N}$ such that $f(a+b+ab)=f(ab)$ , for all $a,b \in \mathbb{N}.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_43083 (f : ℕ → ℕ): (∀ a b : ℕ, f (a + b + a*b) = f (a*b)) ↔ ∃ c :ℕ, ∀ n : ℕ, f n = c   :=  by sorry

Source