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
.
Coercion ℕ → ℤ→ ℤ
as a RingHom
.
Equations
@[simp]
@[simp]
theorem
Int.cast_ite
{α : Type u_1}
[inst : AddGroupWithOne α]
(P : Prop)
[inst : Decidable P]
(m : ℤ)
(n : ℤ)
:
↑(if P then m else n) = if P then ↑m else ↑n
coe : ℤ → α→ α
as an AddMonoidHom
.
@[simp]
theorem
Int.coe_castAddHom
{α : Type u_1}
[inst : AddGroupWithOne α]
:
↑(Int.castAddHom α) = fun x => ↑x
coe : ℤ → α→ α
as a RingHom
.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Int.coe_castRingHom
{α : Type u_1}
[inst : NonAssocRing α]
:
↑(Int.castRingHom α) = fun x => ↑x
@[simp]
@[simp]
theorem
Int.cast_strictMono
{α : Type u_1}
[inst : OrderedRing α]
[inst : Nontrivial α]
:
StrictMono fun x => ↑x
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Int.cast_one_le_of_pos
{α : Type u_1}
[inst : LinearOrderedRing α]
{a : ℤ}
(h : 0 < a)
:
1 ≤ ↑a
theorem
Int.cast_le_neg_one_of_neg
{α : Type u_1}
[inst : LinearOrderedRing α]
{a : ℤ}
(h : a < 0)
:
theorem
Int.cast_natAbs
{α : Type u_1}
[inst : LinearOrderedRing α]
(n : ℤ)
:
↑(Int.natAbs n) = ↑(abs n)
theorem
AddMonoidHom.eq_int_castAddHom
{A : Type u_1}
[inst : AddGroupWithOne A]
(f : ℤ →+ A)
(h1 : ↑f 1 = 1)
:
f = Int.castAddHom A
theorem
eq_intCast'
{F : Type u_2}
{α : Type u_1}
[inst : AddGroupWithOne α]
[inst : AddMonoidHomClass F ℤ α]
(f : F)
(h₁ : ↑f 1 = 1)
(n : ℤ)
:
↑f n = ↑n
theorem
MonoidHom.ext_mint
{M : Type u_1}
[inst : Monoid M]
{f : Multiplicative ℤ →* M}
{g : Multiplicative ℤ →* M}
(h1 : ↑f (↑Multiplicative.ofAdd 1) = ↑g (↑Multiplicative.ofAdd 1))
:
f = g
theorem
MonoidHom.ext_int
{M : Type u_1}
[inst : Monoid M]
{f : ℤ →* M}
{g : ℤ →* M}
(h_neg_one : ↑f (-1) = ↑g (-1))
(h_nat : MonoidHom.comp f ↑Int.ofNatHom = MonoidHom.comp g ↑Int.ofNatHom)
:
f = g
If two MonoidHom
s agree on -1
and the naturals then they are equal.
theorem
MonoidWithZeroHom.ext_int
{M : Type u_1}
[inst : MonoidWithZero M]
{f : ℤ →*₀ M}
{g : ℤ →*₀ M}
(h_neg_one : ↑f (-1) = ↑g (-1))
(h_nat : MonoidWithZeroHom.comp f (RingHom.toMonoidWithZeroHom Int.ofNatHom) = MonoidWithZeroHom.comp g (RingHom.toMonoidWithZeroHom Int.ofNatHom))
:
f = g
If two MonoidWithZeroHom
s agree on -1
and the naturals then they are equal.
theorem
ext_int'
{F : Type u_2}
{α : Type u_1}
[inst : MonoidWithZero α]
[inst : MonoidWithZeroHomClass F ℤ α]
{f : F}
{g : F}
(h_neg_one : ↑f (-1) = ↑g (-1))
(h_pos : ∀ (n : ℕ), 0 < n → ↑f ↑n = ↑g ↑n)
:
f = g
If two MonoidWithZeroHom
s agree on -1
and the positive naturals then they are equal.
@[simp]
theorem
eq_intCast
{F : Type u_1}
{α : Type u_2}
[inst : NonAssocRing α]
[inst : RingHomClass F ℤ α]
(f : F)
(n : ℤ)
:
↑f n = ↑n
@[simp]
theorem
map_intCast
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[inst : NonAssocRing α]
[inst : NonAssocRing β]
[inst : RingHomClass F α β]
(f : F)
(n : ℤ)
:
↑f ↑n = ↑n
theorem
RingHom.eq_intCast'
{α : Type u_1}
[inst : NonAssocRing α]
(f : ℤ →+* α)
:
f = Int.castRingHom α
theorem
RingHom.ext_int
{R : Type u_1}
[inst : NonAssocSemiring R]
(f : ℤ →+* R)
(g : ℤ →+* R)
:
f = g
instance
RingHom.Int.subsingleton_ringHom
{R : Type u_1}
[inst : NonAssocSemiring R]
:
Subsingleton (ℤ →+* R)
Order dual #
Equations
- instAddGroupWithOneOrderDual = h
Equations
- instAddCommGroupWithOneOrderDual = h
Lexicographic order #
Equations
- instAddGroupWithOneLex = h
Equations
- instAddCommGroupWithOneLex = h