mathlib docs: data.int.cast

source

@[simp]

theorem int.nat_cast_eq_coe_nat (n : ℕ) :

↑n = ↑n

source

def int.of_nat_hom :

ℕ →+* ℤ

Coercion ℕ → ℤ as a ring_hom.

Equations

int.of_nat_hom = {to_fun := coe coe_to_lift, map_one' := int.of_nat_hom._proof_1, map_mul' := int.of_nat_mul, map_zero' := int.of_nat_hom._proof_2, map_add' := int.of_nat_add}

source

def int.cast {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] (a : ℤ) :

α

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

Equations

-[1+ n].cast = -(↑n + 1)
↑n.cast = ↑n

source

@[instance]

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

has_coe_t ℤ α

Equations

int.cast_coe = {coe := int.cast _inst_4}

source

@[simp]

theorem int.cast_zero {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :

↑0 = 0

source

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

↑(int.of_nat n) = ↑n

source

@[simp]

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

↑↑n = ↑n

source

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

↑↑n = ↑n

source

@[simp]

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

↑-[1+ n] = -(↑n + 1)

source

@[simp]

theorem int.cast_one {α : Type u_1} [add_monoid α] [has_one α] [has_neg α] :

↑1 = 1

source

@[simp]

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

↑(int.sub_nat_nat m n) = ↑m - ↑n

source

@[simp]

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

↑(int.neg_of_nat n) = -↑n

source

@[simp]

theorem int.cast_add {α : Type u_1} [add_group α] [has_one α] (m n : ℤ) :

↑(m + n) = ↑m + ↑n

source

@[simp]

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

↑-n = -↑n

source

@[simp]

theorem int.cast_sub {α : Type u_1} [add_group α] [has_one α] (m n : ℤ) :

↑(m - n) = ↑m - ↑n

source

@[simp]

theorem int.cast_mul {α : Type u_1} [ring α] (m n : ℤ) :

↑m * n = (↑m) * ↑n

source

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

ℤ →+ α

coe : ℤ → α as an add_monoid_hom.

Equations

int.cast_add_hom α = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}

source

@[simp]

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

⇑(int.cast_add_hom α) = coe

source

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

ℤ →+* α

coe : ℤ → α as a ring_hom.

Equations

int.cast_ring_hom α = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

@[simp]

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

⇑(int.cast_ring_hom α) = coe

source

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

commute ↑m x

source

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

commute x ↑m

source

@[simp]

theorem int.coe_nat_bit0 (n : ℕ) :

↑(bit0 n) = bit0 ↑n

source

@[simp]

theorem int.coe_nat_bit1 (n : ℕ) :

↑(bit1 n) = bit1 ↑n

source

@[simp]

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

↑(bit0 n) = bit0 ↑n

source

@[simp]

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

↑(bit1 n) = bit1 ↑n

source

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

↑2 = 2

source

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

0 ≤ ↑n ↔ 0 ≤ n

source

@[simp]

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

↑m ≤ ↑n ↔ m ≤ n

source

@[simp]

theorem int.cast_lt {α : Type u_1} [linear_ordered_ring α] {m n : ℤ} :

↑m < ↑n ↔ m < n

source

@[simp]

theorem int.cast_nonpos {α : Type u_1} [linear_ordered_ring α] {n : ℤ} :

↑n ≤ 0 ↔ n ≤ 0

source

@[simp]

theorem int.cast_pos {α : Type u_1} [linear_ordered_ring α] {n : ℤ} :

0 < ↑n ↔ 0 < n

source

@[simp]

theorem int.cast_lt_zero {α : Type u_1} [linear_ordered_ring α] {n : ℤ} :

↑n < 0 ↔ n < 0

source

@[simp]

theorem int.cast_min {α : Type u_1} [decidable_linear_ordered_comm_ring α] {a b : ℤ} :

↑(min a b) = min ↑a ↑b

source

@[simp]

theorem int.cast_max {α : Type u_1} [decidable_linear_ordered_comm_ring α] {a b : ℤ} :

↑(max a b) = max ↑a ↑b

source

@[simp]

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

↑(abs q) = abs ↑q

source

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

↑m ∣ ↑n

source

@[ext]

theorem add_monoid_hom.ext_int {A : Type u_1} [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.

source

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

f = int.cast_add_hom A

source

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

source

theorem monoid_hom.ext_int {M : Type u_1} [monoid M] {f g : multiplicative ℤ →* M} (h1 : ⇑f (multiplicative.of_add 1) = ⇑g (multiplicative.of_add 1)) :

f = g

source

@[simp]

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

⇑f n = ↑n

source

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

f = int.cast_ring_hom α

source

@[simp]

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

⇑f ↑n = ↑n

source

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

f = g

source

@[instance]

def ring_hom.int.subsingleton_ring_hom {R : Type u_1} [semiring R] :

subsingleton (ℤ →+* R)

source

@[simp]

theorem int.cast_id (n : ℤ) :

↑n = n