Prove2Me

lean_workbook_plus_63428

Proved

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

For injectivity: ∀m,n∈Z; r,s∈[0,a)\forall m,n\in\mathbb Z;\ r,s\in[0,a) such that fa(n,r)=fa(m,s).f_a(n,r)=f_a(m,s). i.e. an+r=am+s,a(n−m)+r−s=0an+r=am+s,a(n-m)+r-s=0 \nIf n≠mn\ne m then ∣a(n−m)∣>∣r−s∣,|a(n-m)|>|r-s|, but ∣a(n−m)∣=∣r−s∣,|a(n-m)|=|r-s|, a contradiction, so n=m,r=s. fan=m,r=s.\ f_a is injective.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_63428  (a : ℤ)
  (f : ℤ → ℕ → ℤ)
  (h₀ : ∀ n r, f n r = n * a + r)
  (h₁ : 0 < a) :
  Function.Injective f   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph