mathlib documentation

data.int.cast

@[simp]
theorem int.nat_cast_eq_coe_nat (n : ) :

Coercion ℕ → ℤ as a ring_hom.

Equations
def int.cast {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :
→ α

Canonical homomorphism from the integers to any ring(-like) structure α

Equations
@[instance]
def int.cast_coe {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :

Equations
@[simp]
theorem int.cast_zero {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :
0 = 0

theorem int.cast_of_nat {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] (n : ) :

@[simp]
theorem int.cast_coe_nat {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] (n : ) :

theorem int.cast_coe_nat' {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] (n : ) :

@[simp]
theorem int.cast_neg_succ_of_nat {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] (n : ) :
-[1+ n] = -(n + 1)

@[simp]
theorem int.cast_one {α : Type u_1} [add_monoid α] [has_one α] [has_neg α] :
1 = 1

@[simp]
theorem int.cast_sub_nat_nat {α : Type u_1} [add_group α] [has_one α] (m n : ) :

@[simp]
theorem int.cast_neg_of_nat {α : Type u_1} [add_group α] [has_one α] (n : ) :

@[simp]
theorem int.cast_add {α : Type u_1} [add_group α] [has_one α] (m n : ) :
(m + n) = m + n

@[simp]
theorem int.cast_neg {α : Type u_1} [add_group α] [has_one α] (n : ) :

@[simp]
theorem int.cast_sub {α : Type u_1} [add_group α] [has_one α] (m n : ) :
(m - n) = m - n

@[simp]
theorem int.cast_mul {α : Type u_1} [ring α] (m n : ) :
m * n = (m) * n

def int.cast_add_hom (α : Type u_1) [add_group α] [has_one α] :

coe : ℤ → α as an add_monoid_hom.

Equations
@[simp]
theorem int.coe_cast_add_hom {α : Type u_1} [add_group α] [has_one α] :

def int.cast_ring_hom (α : Type u_1) [ring α] :

coe : ℤ → α as a ring_hom.

Equations
@[simp]
theorem int.coe_cast_ring_hom {α : Type u_1} [ring α] :

theorem int.cast_commute {α : Type u_1} [ring α] (m : ) (x : α) :

theorem int.commute_cast {α : Type u_1} [ring α] (x : α) (m : ) :

@[simp]
theorem int.coe_nat_bit0 (n : ) :

@[simp]
theorem int.coe_nat_bit1 (n : ) :

@[simp]
theorem int.cast_bit0 {α : Type u_1} [ring α] (n : ) :

@[simp]
theorem int.cast_bit1 {α : Type u_1} [ring α] (n : ) :

theorem int.cast_two {α : Type u_1} [ring α] :
2 = 2

theorem int.cast_nonneg {α : Type u_1} [linear_ordered_ring α] {n : } :
0 n 0 n

@[simp]
theorem int.cast_le {α : Type u_1} [linear_ordered_ring α] {m n : } :
m n m n

@[simp]
theorem int.cast_lt {α : Type u_1} [linear_ordered_ring α] {m n : } :
m < n m < n

@[simp]
theorem int.cast_nonpos {α : Type u_1} [linear_ordered_ring α] {n : } :
n 0 n 0

@[simp]
theorem int.cast_pos {α : Type u_1} [linear_ordered_ring α] {n : } :
0 < n 0 < n

@[simp]
theorem int.cast_lt_zero {α : Type u_1} [linear_ordered_ring α] {n : } :
n < 0 n < 0

@[simp]
theorem int.cast_min {α : Type u_1} [decidable_linear_ordered_comm_ring α] {a b : } :
(min a b) = min a b

@[simp]
theorem int.cast_max {α : Type u_1} [decidable_linear_ordered_comm_ring α] {a b : } :
(max a b) = max a b

@[simp]
theorem int.cast_abs {α : Type u_1} [decidable_linear_ordered_comm_ring α] {q : } :

theorem int.coe_int_dvd {α : Type u_1} [comm_ring α] (m n : ) :
m nm n

@[ext]
theorem add_monoid_hom.ext_int {A : Type u_1} [add_monoid A] {f g : →+ A} :
f 1 = g 1f = 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_1} [add_group A] [has_one A] (f : →+ A) :
f 1 = 1f = int.cast_add_hom A

theorem add_monoid_hom.eq_int_cast {A : Type u_1} [add_group A] [has_one A] (f : →+ A) (h1 : f 1 = 1) (n : ) :
f n = n

@[simp]
theorem ring_hom.eq_int_cast {α : Type u_1} [ring α] (f : →+* α) (n : ) :
f n = n

theorem ring_hom.eq_int_cast' {α : Type u_1} [ring α] (f : →+* α) :

@[simp]
theorem ring_hom.map_int_cast {α : Type u_1} {β : Type u_2} [ring α] [ring β] (f : α →+* β) (n : ) :

theorem ring_hom.ext_int {R : Type u_1} [semiring R] (f g : →+* R) :
f = g

@[instance]

@[simp]
theorem int.cast_id (n : ) :
n = n