English
There is a canonical equivalence between the set of associates of ℤ and ℕ given by the natAbs map.
Русский
Существует каноническое эквивалентное отображение между множествами ассоциатов ℤ и ℕ, задаваемое natAbs.
LaTeX
$$$\text{associates}(\mathbb{Z}) \simeq \mathbb{N}$, определяемое $[a] \mapsto |a|$$$
Lean4
/-- Maps an associate class of integers consisting of `-n, n` to `n : ℕ` -/
def associatesIntEquivNat : Associates ℤ ≃ ℕ :=
by
refine ⟨(·.out.natAbs), (Associates.mk ·), ?_, fun n ↦ ?_⟩
· refine Associates.forall_associated.2 fun a ↦ ?_
refine Associates.mk_eq_mk_iff_associated.2 <| Associated.symm <| ⟨normUnit a, ?_⟩
simp [Int.natCast_natAbs, Int.abs_eq_normalize, normalize_apply]
· dsimp only [Associates.out_mk]
rw [← Int.abs_eq_normalize, Int.natAbs_abs, Int.natAbs_natCast]
