Cast of integers (additional theorems) #
This file proves additional properties about the canonical homomorphism from
the integers into an additive group with a one (Int.cast
).
There is also Mathlib.Data.Int.Cast.Lemmas
,
which includes lemmas stated in terms of algebraic homomorphisms,
and results involving the order structure of ℤ
.
By contrast, this file's only import beyond Mathlib.Data.Int.Cast.Defs
is
Mathlib.Algebra.Group.Basic
.
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]