English
There is an equivalence between the natural numbers and Nat × Fin n given a nonzero n: a ↦ (a/n, a mod n) with inverse (q,r) ↦ q·n + r.
Русский
Существует эквивалентность между натуральными числами и Nat × Fin(n) при не нулевом n: a ↦ (a/n, a mod n) и обратное (q,r) ↦ q·n + r.
LaTeX
$$$ Nat \\cong Nat \\times Fin(n) $ with $(a) \\mapsto (a/n, \\mathrm{Fin.ofNat}(n, a \\bmod n))$ and inverse $(q,r) \\mapsto q\\,n + r$$$
Lean4
/-- The equivalence induced by `a ↦ (a / n, a % n)` for nonzero `n`.
This is like `finProdFinEquiv.symm` but with `m` infinite.
See `Nat.div_mod_unique` for a similar propositional statement. -/
@[simps]
def divModEquiv (n : ℕ) [NeZero n] : ℕ ≃ ℕ × Fin n
where
toFun a := (a / n, Fin.ofNat n a)
invFun
p :=
p.1 * n +
↑p.2
-- TODO: is there a canonical order of `*` and `+` here?
left_inv _ := Nat.div_add_mod' _ _
right_inv
p := by
refine Prod.ext ?_ (Fin.ext <| Nat.mul_add_mod_of_lt p.2.is_lt)
dsimp only
rw [Nat.add_comm, Nat.add_mul_div_right _ _ n.pos_of_neZero, Nat.div_eq_of_lt p.2.is_lt, Nat.zero_add]
