lean_workbook_plus_24925

Disproved

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

Hence $f(n)=nf(1)$ so $f(f(n))=n=f(n)f(1)=nf(1)^2$ so $f(1)^2=1\implies f(1)=1$ so $\boxed{f(n)=n}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24925  (n : ℕ)
  (f : ℕ → ℕ)
  (h₀ : ∃ n, f n ≠ n)
  (h₁ : ∀ n, f (f n) = n * f 1)
  (h₂ : ∃ n, f n ≠ n * f 1) :
  f 1 = 1 ∧ ∀ n, f n = n   :=  by sorry

Source

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

View graph