lean_workbook_plus_31350

Proved

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

$f(1) = f(0) + 1$ and $f(1) = f(1)^3, f(0) = f(0)^3$ , from which we conclude that $f(0) = 0, f(1) = 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_31350 (f : ℕ → ℕ) (hf₁ : f 1 = f 0 + 1) (hf₂ : f 1 = (f 1)^3) (hf₃ : f 0 = (f 0)^3) : f 0 = 0 ∧ f 1 = 1   :=  by sorry

Source