Cast of integers (additional theorems) #
This file proves additional properties about the canonical homomorphism from
the integers into an additive group with a one (
particularly results involving algebraic homomorphisms or the order structure on
which were not available in the import dependencies of
Main declarations #
MonoidWithZeroHoms agree on
-1 and the naturals then they are equal.