Coercion ℕ → ℤ as a ring_hom.
ℕ → ℤ
Canonical homomorphism from the integers to any ring(-like) structure α
coe : ℤ → α as an add_monoid_hom.
coe : ℤ → α
coe : ℤ → α as a ring_hom.
Two additive monoid homomorphisms f, g from ℤ to an additive monoid are equal
if f 1 = g 1.
f 1 = g 1