mathlib documentation

data.int.cast.lemmas

Cast of integers (additional theorems) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Coercion ℕ → ℤ as a ring_hom.

Equations
@[simp]
theorem int.coe_nat_pos {n : } :
0 < n 0 < n
theorem int.coe_nat_succ_pos (n : ) :
0 < (n.succ)
theorem int.to_nat_lt {a : } {b : } (hb : b 0) :
a.to_nat < b a < b
theorem int.nat_mod_lt {a : } {b : } (hb : b 0) :
@[simp, norm_cast]
theorem int.cast_mul {α : Type u_3} [non_assoc_ring α] (m n : ) :
(m * n) = m * n
@[simp, norm_cast]
theorem int.cast_ite {α : Type u_3} [add_group_with_one α] (P : Prop) [decidable P] (m n : ) :
(ite P m n) = ite P m n
def int.cast_add_hom (α : Type u_1) [add_group_with_one α] :

coe : ℤ → α as an add_monoid_hom.

Equations
@[simp]
def int.cast_ring_hom (α : Type u_1) [non_assoc_ring α] :

coe : ℤ → α as a ring_hom.

Equations
@[simp]
theorem int.cast_commute {α : Type u_3} [non_assoc_ring α] (m : ) (x : α) :
theorem int.cast_comm {α : Type u_3} [non_assoc_ring α] (m : ) (x : α) :
m * x = x * m
theorem int.commute_cast {α : Type u_3} [non_assoc_ring α] (x : α) (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
@[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]
@[simp, norm_cast]
@[simp, norm_cast]
theorem int.cast_abs {α : Type u_3} [linear_ordered_ring α] {a : } :
theorem int.cast_one_le_of_pos {α : Type u_3} [linear_ordered_ring α] {a : } (h : 0 < a) :
1 a
theorem int.cast_le_neg_one_of_neg {α : Type u_3} [linear_ordered_ring α] {a : } (h : a < 0) :
a -1
theorem int.nneg_mul_add_sq_of_abs_le_one {α : Type u_3} [linear_ordered_ring α] (n : ) {x : α} (hx : |x| 1) :
0 n * x + n * n
theorem int.cast_nat_abs {α : Type u_3} [linear_ordered_ring α] (n : ) :
theorem int.coe_int_dvd {α : Type u_3} [comm_ring α] (m n : ) (h : m 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} [add_group_with_one A] (f : →+ A) (h1 : f 1 = 1) :
theorem eq_int_cast' {F : Type u_1} {α : Type u_3} [add_group_with_one α] [add_monoid_hom_class F α] (f : F) (h₁ : f 1 = 1) (n : ) :
f n = n
@[ext]
@[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.comp int.of_nat_hom.to_monoid_hom = g.comp int.of_nat_hom.to_monoid_hom) :
f = g

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

@[ext]

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} [monoid_with_zero α] [monoid_with_zero_hom_class F α] {f g : F} (h_neg_one : f (-1) = g (-1)) (h_pos : (n : ), 0 < n f 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} [non_assoc_ring α] [ring_hom_class F α] (f : F) (n : ) :
f n = n
@[simp]
theorem map_int_cast {F : Type u_1} {α : Type u_3} {β : Type u_4} [non_assoc_ring α] [non_assoc_ring β] [ring_hom_class F α β] (f : F) (n : ) :
theorem ring_hom.eq_int_cast' {α : Type u_3} [non_assoc_ring α] (f : →+* α) :
theorem ring_hom.ext_int {R : Type u_1} [non_assoc_semiring R] (f g : →+* R) :
f = g
@[protected, instance]
@[simp, norm_cast]
theorem int.cast_id (n : ) :
n = n
@[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 : ) :
@[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]
@[simp, norm_cast]

Order dual #

@[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]
Equations
@[protected, instance]
Equations
@[simp]
theorem to_lex_int_cast {α : Type u_3} [has_int_cast α] (n : ) :
@[simp]
theorem of_lex_int_cast {α : Type u_3} [has_int_cast α] (n : ) :