lean_workbook_plus_65467

Proved

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

I've got these things: $f(p-1)=p-1$ for all primes $p$ . $f(n)\leq{n}$ for all positive integers.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_65467 {f : ℕ → ℕ} (hf : ∀ p, Nat.Prime p → f (p - 1) = p - 1) (hf_le : ∀ n, f n ≤ n) : f 1 = 1   :=  by sorry

Source