lean_workbook_plus_22341

Proved

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

Being a function linear we have that

\frac{f(n)}{n} = k

, with k constant, on the other hand the expression is equivalent to

\frac{f(x ^ 2-y ^ 2)}{x ^ 2-y ^ 2} = \frac {f(x)}{x}. \frac{f(2y)}{2y}

, then $k = k ^ 2$ , then k∈ {0, 1}, if k = 0, then $f (n) = 0$ , If k = 1 then, $f (n) = n$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_22341  (f : ℤ → ℤ)
  (h₀ : ∃ k, ∀ n, f n = k * n)
  (h₁ : ∀ x y, f (x^2 - y^2) = f x * f (2 * y)) :
  ∀ n, f n = 0 ∨ ∀ n, f n = n   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph