lean_workbook_plus_52965

Proved

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

Let $S=\{1, 2,3, \cdots, 12\}$ . How many functions $f: S \rightarrow S$ are there such that $f(f(x))=x$ and $f(x)-x$ is divisible by 3 ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_52965 (S : Finset ℕ) (hS : S = Finset.Icc 1 12) : ∃ f : ℕ → ℕ, ∀ x ∈ S, f (f x) = x ∧ (f x - x) % 3 = 0   :=  by sorry

Source