by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
We note that f(ka)=kf(a) for all positive integers k by writing f(ka)=f(a+a+a+....+a)=f(a)+f(a+a+..+a)=f(a)+f(a)+f(a+a+...+a)=... , where each step removes one a from inside the function and adds an f(a) outside the bracket. \n\nThus, f(2008)=2008⋅f(1) , and f(2009)=2009⋅f(1) . \n\nTherefore, f(1)=2008f(2008)=2009f(2009) . Plug-n-chug from there.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_55691 (f : ℕ → ℕ)
(h₀ : ∀ k, 0 < k → ∀ a, f (k * a) = k * f a)
: f 1 = f 2008 / 2008 ∧ f 1 = f 2009 / 2009 := by sorry