English
There is a natural bijection between ℕ and ZMod N × ℕ given by n ↦ (n mod N, n / N) with inverse (r,q) ↦ r + N·q.
Русский
Существует биекция между ℕ и ZMod N × ℕ, заданная отображением n ↦ (n mod N, n / N) и обратным отображением (r, q) ↦ r + N·q.
LaTeX
$$$\mathbb{N} \cong \mathbb{Z}/N\mathbb{Z} \times \mathbb{N}$ via $n \mapsto (n \bmod N, \lfloor n / N \rfloor)$$$
Lean4
/-- Equivalence between `ℕ` and `ZMod N × ℕ`, sending `n` to `(n mod N, n / N)`. -/
def residueClassesEquiv (N : ℕ) [NeZero N] : ℕ ≃ ZMod N × ℕ
where
toFun n := (↑n, n / N)
invFun p := p.1.val + N * p.2
left_inv n := by simpa only [val_natCast] using mod_add_div n N
right_inv
p := by
ext1
· simp only [add_comm p.1.val, cast_add, cast_mul, natCast_self, zero_mul, natCast_val, cast_id', id_eq, zero_add]
· simp only [add_comm p.1.val, mul_add_div (NeZero.pos _), (Nat.div_eq_zero_iff).2 <| .inr p.1.val_lt, add_zero]
