English
There is a canonical morphism from ℤ to any abelian group G sending 1 to a given element g of G; i.e., for each g ∈ G there is a unique morphism ⟨ℤ → G⟩ with 1 ↦ g.
Русский
Существует канонический мороморфизм из ℤ в любую абелеву группу G, отправляющий 1 в данное элемент g ∈ G; т.е. для каждого g ∈ G существует уникальный мороморфизм ℤ → G с образом 1 равным g.
LaTeX
$$$$ \forall G \ (g \in G),\ \exists! f: \mathbb{Z} \to G \text{ such that } f(1) = g. $$$$
Lean4
/-- Any element of an abelian group gives a unique morphism from `ℤ` sending
`1` to that element. -/
@[simps!]
def asHom {G : AddCommGrpCat.{0}} (g : G) : AddCommGrpCat.of ℤ ⟶ G :=
ofHom (zmultiplesHom G g)
