Cast of integers (additional theorems) #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file proves additional properties about the canonical homomorphism from
the integers into an additive group with a one (
There is also
which includes lemmas stated in terms of algebraic homomorphisms,
and results involving the order structure of
By contrast, this file's only import beyond