lean_workbook_plus_37880
ProvedLet . Find the number of one-to-one function satisfying following condition: for all , is not a multiple of .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_37880 (A: Finset ℕ) (hA: A = Finset.Icc 1 12): ∃ f : ℕ → ℕ, Function.Injective f ∧ ∀ i ∈ A, ¬ 3 ∣ (f i - i) := by sorry
Source