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
),
particularly results involving algebraic homomorphisms or the order structure on ℤ
which were not available in the import dependencies of Data.Int.Cast.Basic
.
Main declarations #
castAddHom
:cast
bundled as anAddMonoidHom
.castRingHom
:cast
bundled as aRingHom
.
coe : ℤ → α
as an AddMonoidHom
.
Equations
- Int.castAddHom α = { toFun := Int.cast, map_zero' := ⋯, map_add' := ⋯ }
Instances For
coe : ℤ → α
as a RingHom
.
Equations
- Int.castRingHom α = { toFun := Int.cast, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Alias of Int.cast_dvd_cast
.
Alias of SemiconjBy.intCast_mul_right
.
Alias of SemiconjBy.intCast_mul_left
.
Alias of SemiconjBy.intCast_mul_intCast_mul
.
Alias of Commute.intCast_right
.
Alias of Commute.intCast_left
.
Alias of Commute.intCast_mul_right
.
Alias of Commute.intCast_mul_left
.
Alias of Commute.intCast_mul_intCast_mul
.
Alias of Commute.self_intCast_mul
.
Alias of Commute.intCast_mul_self
.
Alias of Commute.self_intCast_mul_intCast_mul
.
Alias of AddMonoidHom.eq_intCastAddHom
.
If two MonoidHom
s agree on -1
and the naturals then they are equal.
If two MonoidWithZeroHom
s agree on -1
and the naturals then they are equal.
If two MonoidWithZeroHom
s agree on -1
and the positive naturals then they are equal.
Additive homomorphisms from ℤ
are defined by the image of 1
.
Equations
Instances For
Monoid homomorphisms from Multiplicative ℤ
are defined by the image
of Multiplicative.ofAdd 1
.
Equations
- zpowersHom α = Additive.ofMul.trans ((zmultiplesHom (Additive α)).trans AddMonoidHom.toMultiplicative'')
Instances For
If α
is commutative, zmultiplesHom
is an additive equivalence.
Equations
- zmultiplesAddHom β = { toEquiv := zmultiplesHom β, map_add' := ⋯ }
Instances For
If α
is commutative, zpowersHom
is a multiplicative equivalence.
Equations
- zpowersMulHom α = { toEquiv := zpowersHom α, map_mul' := ⋯ }