lean_workbook_plus_53583

Proved

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

Find all functions $f:N->N$ such that $(n-1)^2 < f(n)f(f(n)) < n^2+n$ for every positive integers $n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_53583 (f : ℕ → ℕ) (hf: ∀ n : ℕ, (n-1)^2 < f n * f (f n) ∧ f n * f (f n) < n^2 + n) : ∀ n : ℕ, f n = n   :=  by sorry

Source