Cast of natural numbers (additional theorems) #
This file proves additional properties about the canonical homomorphism from
the natural numbers into an additive monoid with a one (Nat.cast
).
Main declarations #
castAddMonoidHom
:cast
bundled as anAddMonoidHom
.castRingHom
:cast
bundled as aRingHom
.