data.int.cast

# 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).

## Main declarations #

• cast_add_hom: cast bundled as an add_monoid_hom.
• cast_ring_hom: cast bundled as a ring_hom.
def int.of_nat_hom  :

Coercion ℕ → ℤ as a ring_hom.

Equations
@[simp, norm_cast]
theorem int.cast_mul {α : Type u_3} (m n : ) :
(m * n) = m * n
@[simp, norm_cast]
theorem int.cast_ite {α : Type u_3} (P : Prop) [decidable P] (m n : ) :
(ite P m n) = ite P m n
def int.cast_add_hom (α : Type u_1)  :

coe : ℤ → α as an add_monoid_hom.

Equations
@[simp]
theorem int.coe_cast_add_hom {α : Type u_3}  :
def int.cast_ring_hom (α : Type u_1)  :

coe : ℤ → α as a ring_hom.

Equations
@[simp]
theorem int.coe_cast_ring_hom {α : Type u_3}  :
theorem int.cast_commute {α : Type u_3} (m : ) (x : α) :
x
theorem int.cast_comm {α : Type u_3} (m : ) (x : α) :
m * x = x * m
theorem int.commute_cast {α : Type u_3} (x : α) (m : ) :
m
theorem int.cast_mono {α : Type u_3} [ordered_ring α] :
@[simp]
theorem int.cast_nonneg {α : Type u_3} [ordered_ring α] [nontrivial α] {n : } :
0 n 0 n
@[simp, norm_cast]
theorem int.cast_le {α : Type u_3} [ordered_ring α] [nontrivial α] {m n : } :
m n m n
theorem int.cast_strict_mono {α : Type u_3} [ordered_ring α] [nontrivial α] :
@[simp, norm_cast]
theorem int.cast_lt {α : Type u_3} [ordered_ring α] [nontrivial α] {m n : } :
m < n m < n
@[simp]
theorem int.cast_nonpos {α : Type u_3} [ordered_ring α] [nontrivial α] {n : } :
n 0 n 0
@[simp]
theorem int.cast_pos {α : Type u_3} [ordered_ring α] [nontrivial α] {n : } :
0 < n 0 < n
@[simp]
theorem int.cast_lt_zero {α : Type u_3} [ordered_ring α] [nontrivial α] {n : } :
n < 0 n < 0
@[simp, norm_cast]
theorem int.cast_min {α : Type u_3} {a b : } :
b) =
@[simp, norm_cast]
theorem int.cast_max {α : Type u_3} {a b : } :
b) =
@[simp, norm_cast]
theorem int.cast_abs {α : Type u_3} {a : } :
theorem int.cast_one_le_of_pos {α : Type u_3} {a : } (h : 0 < a) :
1 a
theorem int.cast_le_neg_one_of_neg {α : Type u_3} {a : } (h : a < 0) :
a -1
theorem int.nneg_mul_add_sq_of_abs_le_one {α : Type u_3} (n : ) {x : α} (hx : |x| 1) :
0 n * x + n * n
theorem int.cast_nat_abs {α : Type u_3} (n : ) :
theorem int.coe_int_dvd {α : Type u_3} [comm_ring α] (m n : ) (h : m n) :
@[protected, instance]
def prod.add_group_with_one {α : Type u_3} {β : Type u_4}  :
Equations
@[simp]
theorem prod.fst_int_cast {α : Type u_3} {β : Type u_4} (n : ) :
@[simp]
theorem prod.snd_int_cast {α : Type u_3} {β : Type u_4} (n : ) :
@[ext]
theorem add_monoid_hom.ext_int {A : Type u_5} [add_monoid A] {f g : →+ A} (h1 : f 1 = g 1) :
f = g

Two additive monoid homomorphisms f, g from ℤ to an additive monoid are equal if f 1 = g 1.

theorem add_monoid_hom.eq_int_cast_hom {A : Type u_5} (f : →+ A) (h1 : f 1 = 1) :
theorem eq_int_cast' {F : Type u_1} {α : Type u_3} [ α] (f : F) (h₁ : f 1 = 1) (n : ) :
f n = n
@[simp]
@[ext]
theorem monoid_hom.ext_mint {M : Type u_5} [monoid M] {f g : →* M} (h1 : = ) :
f = g
@[ext]
theorem monoid_hom.ext_int {M : Type u_5} [monoid M] {f g : →* M} (h_neg_one : f (-1) = g (-1)) (h_nat : = ) :
f = g

If two monoid_homs agree on -1 and the naturals then they are equal.

@[ext]
theorem monoid_with_zero_hom.ext_int {M : Type u_5} {f g : →*₀ M} (h_neg_one : f (-1) = g (-1))  :
f = g

If two monoid_with_zero_homs agree on -1 and the naturals then they are equal.

theorem ext_int' {F : Type u_1} {α : Type u_3} {f g : F} (h_neg_one : f (-1) = g (-1)) (h_pos : ∀ (n : ), 0 < nf n = g n) :
f = g

If two monoid_with_zero_homs agree on -1 and the positive naturals then they are equal.

@[simp]
theorem eq_int_cast {F : Type u_1} {α : Type u_3} [ α] (f : F) (n : ) :
f n = n
@[simp]
theorem map_int_cast {F : Type u_1} {α : Type u_3} {β : Type u_4} [ β] (f : F) (n : ) :
theorem ring_hom.eq_int_cast' {α : Type u_3} (f : →+* α) :
theorem ring_hom.ext_int {R : Type u_1} (f g : →+* R) :
f = g
@[protected, instance]
@[simp, norm_cast]
theorem int.cast_id (n : ) :
n = n
@[simp]
@[protected, instance]
def pi.has_int_cast {ι : Type u_2} {π : ι → Type u_5} [Π (i : ι), has_int_cast (π i)] :
has_int_cast (Π (i : ι), π i)
Equations
theorem pi.int_apply {ι : Type u_2} {π : ι → Type u_5} [Π (i : ι), has_int_cast (π i)] (n : ) (i : ι) :
n i = n
@[simp]
theorem pi.coe_int {ι : Type u_2} {π : ι → Type u_5} [Π (i : ι), has_int_cast (π i)] (n : ) :
n = λ (_x : ι), n
theorem sum.elim_int_cast_int_cast {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_int_cast γ] (n : ) :
n = n
@[protected, instance]
def pi.add_group_with_one {ι : Type u_2} {π : ι → Type u_5} [Π (i : ι), add_group_with_one (π i)] :
add_group_with_one (Π (i : ι), π i)
Equations
@[simp, norm_cast]
theorem mul_opposite.op_int_cast {α : Type u_3} (z : ) :
@[simp, norm_cast]
theorem mul_opposite.unop_int_cast {α : Type u_3} (n : ) :

### Order dual #

@[protected, instance]
def order_dual.has_int_cast {α : Type u_3} [h : has_int_cast α] :
Equations
@[protected, instance]
def order_dual.add_group_with_one {α : Type u_3} [h : add_group_with_one α] :
Equations
@[protected, instance]
Equations
@[simp]
theorem to_dual_int_cast {α : Type u_3} [has_int_cast α] (n : ) :
@[simp]
theorem of_dual_int_cast {α : Type u_3} [has_int_cast α] (n : ) :

### Lexicographic order #

@[protected, instance]
def lex.has_int_cast {α : Type u_3} [h : has_int_cast α] :
Equations
@[protected, instance]
def lex.add_group_with_one {α : Type u_3} [h : add_group_with_one α] :
Equations
@[protected, instance]
def lex.add_comm_group_with_one {α : Type u_3} [h : add_comm_group_with_one α] :
Equations
@[simp]
theorem to_lex_int_cast {α : Type u_3} [has_int_cast α] (n : ) :
= n
@[simp]
theorem of_lex_int_cast {α : Type u_3} [has_int_cast α] (n : ) :