Canonical homomorphism from ℕ to a type α with 0, 1 and +.
Computationally friendlier cast than nat.cast, using binary representation.
coe : ℕ → α as an add_monoid_hom.
coe : ℕ → α
coe : ℕ → α as a ring_hom
Alias of coe_nat_dvd.
If two monoid_with_zero_homs agree on the positive naturals they are equal.