lean_workbook_plus_67533

Proved

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

Determine all solutions $f: \mathbb{N} \to \mathbb{N}$ of the functional equation \n\n $f(n+m)=f(n)+f(m),$ \n\nfor all $m,n \in \mathbb{N}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67533 (f : ℕ → ℕ): (∀ m n: ℕ, f (m + n) = f m + f n) ↔ ∃ a: ℕ, ∀ n: ℕ, f n = a * n   :=  by sorry

Source