lean_workbook_plus_61776

Disproved

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

Prove that this function is multiplicative: $f(m+n) = f(m)f(n)$ for all $n,m \epsilon N$ (i) $f(0)=0$ (ii) $f(1)=1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_61776 (f : ℕ → ℕ) (i : f 0 = 0) (ii : f 1 = 1) : ∀ n m : ℕ, f (m + n) = f m * f n   :=  by sorry

Source