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
.
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
SemiconjBy.intCast_mul_right
{α : Type u_3}
[Ring α]
{a x y : α}
(h : SemiconjBy a x y)
(n : ℤ)
:
SemiconjBy a (↑n * x) (↑n * y)
@[simp]
theorem
SemiconjBy.intCast_mul_left
{α : Type u_3}
[Ring α]
{a x y : α}
(h : SemiconjBy a x y)
(n : ℤ)
:
SemiconjBy (↑n * a) x y
theorem
SemiconjBy.intCast_mul_intCast_mul
{α : Type u_3}
[Ring α]
{a x y : α}
(h : SemiconjBy a x y)
(m n : ℤ)
:
SemiconjBy (↑m * a) (↑n * x) (↑n * y)
@[simp]
@[simp]
theorem
AddMonoidHom.eq_intCastAddHom
{A : Type u_5}
[AddGroupWithOne A]
(f : ℤ →+ A)
(h1 : f 1 = 1)
:
theorem
eq_intCast'
{F : Type u_1}
{α : Type u_3}
[AddGroupWithOne α]
[FunLike F ℤ α]
[AddMonoidHomClass F ℤ α]
(f : F)
(h₁ : f 1 = 1)
(n : ℤ)
:
theorem
map_intCast'
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[AddGroupWithOne α]
[AddGroupWithOne β]
[FunLike F α β]
[AddMonoidHomClass F α β]
(f : F)
(h₁ : f 1 = 1)
(n : ℤ)
:
This version is primed so that the RingHomClass
versions aren't.
theorem
MonoidHom.ext_mint
{M : Type u_5}
[Monoid M]
{f g : Multiplicative ℤ →* M}
(h1 : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1))
:
theorem
MonoidHom.ext_int
{M : Type u_5}
[Monoid M]
{f g : ℤ →* M}
(h_neg_one : f (-1) = g (-1))
(h_nat : f.comp ↑Int.ofNatHom = g.comp ↑Int.ofNatHom)
:
If two MonoidHom
s agree on -1
and the naturals then they are equal.
theorem
MonoidWithZeroHom.ext_int
{M : Type u_5}
[MonoidWithZero M]
{f g : ℤ →*₀ M}
(h_neg_one : f (-1) = g (-1))
(h_nat : f.comp Int.ofNatHom.toMonoidWithZeroHom = g.comp Int.ofNatHom.toMonoidWithZeroHom)
:
If two MonoidWithZeroHom
s agree on -1
and the naturals then they are equal.
theorem
MonoidWithZeroHom.ext_int_iff
{M : Type u_5}
[MonoidWithZero M]
{f g : ℤ →*₀ M}
:
f = g ↔ f (-1) = g (-1) ∧ f.comp Int.ofNatHom.toMonoidWithZeroHom = g.comp Int.ofNatHom.toMonoidWithZeroHom
theorem
ext_int'
{F : Type u_1}
{α : Type u_3}
[MonoidWithZero α]
[FunLike F ℤ α]
[MonoidWithZeroHomClass F ℤ α]
{f g : F}
(h_neg_one : f (-1) = g (-1))
(h_pos : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n)
:
If two MonoidWithZeroHom
s agree on -1
and the positive naturals then they are equal.
Monoid homomorphisms from Multiplicative ℤ
are defined by the image
of Multiplicative.ofAdd 1
.
Equations
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
theorem
MonoidHom.apply_mint
(α : Type u_3)
[Group α]
(f : Multiplicative ℤ →* α)
(n : Multiplicative ℤ)
:
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
eq_intCast
{F : Type u_1}
{α : Type u_3}
[NonAssocRing α]
[FunLike F ℤ α]
[RingHomClass F ℤ α]
(f : F)
(n : ℤ)
:
@[simp]
theorem
map_intCast
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[NonAssocRing α]
[NonAssocRing β]
[FunLike F α β]
[RingHomClass F α β]
(f : F)
(n : ℤ)
:
instance
RingHom.Int.subsingleton_ringHom
{R : Type u_5}
[NonAssocSemiring R]
:
Subsingleton (ℤ →+* R)