English
There is a natural bijection between elements of M and additive monoid homomorphisms from ℕ to M, given by x ↦ (n ↦ n • x) and inverse f ↦ f(1).
Русский
Существует естественная биекция между элементами M и аддитивными моноид-гомоморфизмами из ℕ в M, заданная отображением x ↦ (n ↦ n • x) и обратным отображением f ↦ f(1).
LaTeX
$$$ M \simeq (\mathbb{N} \to_+ M)$$$
Lean4
/-- Additive homomorphisms from `ℕ` are defined by the image of `1`. -/
def multiplesHom : M ≃ (ℕ →+ M)
where
toFun
x :=
{ toFun := fun n ↦ n • x
map_zero' := zero_nsmul x
map_add' := fun _ _ ↦ add_nsmul _ _ _ }
invFun f := f 1
left_inv := one_nsmul
right_inv f := AddMonoidHom.ext_nat <| one_nsmul (f 1)
