mathlib documentation

data.int.cast

Cast of integers #

This file defines the canonical homomorphism from the integers into a type α with 0, 1, + and - (typically a ring).

Main declarations #

cast: Canonical homomorphism ℤ → α where α has a 0, 1, + and -.
cast_add_hom: cast bundled as an add_monoid_hom.
cast_ring_hom: cast bundled as a ring_hom.

Implementation note #

Setting up the coercions priorities is tricky. See Note [coercion into rings].

@[simp]

theorem int.nat_cast_eq_coe_nat (n : ℕ) :

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}

@[protected]

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

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

@[protected, 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}

@[simp, norm_cast]

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 : ℕ) :

↑(int.of_nat n) = ↑n

@[simp, norm_cast]

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, norm_cast]

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

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

@[simp, norm_cast]

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 : ℕ) :

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

@[simp, norm_cast]

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

↑(int.neg_of_nat n) = -↑n

@[simp, norm_cast]

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

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

@[simp, norm_cast]

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

@[simp, norm_cast]

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

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

@[simp, norm_cast]

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

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

@[simp]

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

⇑(int.cast_add_hom α) = coe

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' := _}

@[simp]

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

⇑(int.cast_ring_hom α) = coe

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

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

(↑m) * x = x * ↑m

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

@[simp, norm_cast]

theorem int.coe_nat_bit0 (n : ℕ) :

↑(bit0 n) = bit0 ↑n

@[simp, norm_cast]

theorem int.coe_nat_bit1 (n : ℕ) :

↑(bit1 n) = bit1 ↑n

@[simp, norm_cast]

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

↑(bit0 n) = bit0 ↑n

@[simp, norm_cast]

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

↑(bit1 n) = bit1 ↑n

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

↑2 = 2

theorem int.cast_mono {α : Type u_1} [ordered_ring α] :

@[simp]

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

0 ≤ ↑n ↔ 0 ≤ n

@[simp, norm_cast]

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

↑m ≤ ↑n ↔ m ≤ n

theorem int.cast_strict_mono {α : Type u_1} [ordered_ring α] [nontrivial α] :

strict_mono coe

@[simp, norm_cast]

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

↑m < ↑n ↔ m < n

@[simp]

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

↑n ≤ 0 ↔ n ≤ 0

@[simp]

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

0 < ↑n ↔ 0 < n

@[simp]

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

↑n < 0 ↔ n < 0

@[simp, norm_cast]

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

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

@[simp, norm_cast]

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

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

@[simp, norm_cast]

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

↑|q| = |↑q|

theorem int.cast_nat_abs {R : Type u_1} [linear_ordered_ring R] (n : ℤ) :

↑(n.nat_abs) = |↑n|

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

@[simp]

theorem prod.fst_int_cast {α : Type u_1} {β : Type u_2} [has_zero α] [has_one α] [has_add α] [has_neg α] [has_zero β] [has_one β] [has_add β] [has_neg β] (n : ℤ) :

↑n.fst = ↑n

@[simp]

theorem prod.snd_int_cast {α : Type u_1} {β : Type u_2} [has_zero α] [has_one α] [has_add α] [has_neg α] [has_zero β] [has_one β] [has_add β] [has_neg β] (n : ℤ) :

↑n.snd = ↑n

@[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.

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

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

@[simp]

theorem int.cast_add_hom_int :

int.cast_add_hom ℤ = add_monoid_hom.id ℤ

@[ext]

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

f = g

@[ext]

theorem monoid_hom.ext_int {M : Type u_1} [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]

theorem monoid_with_zero_hom.ext_int {M : Type u_1} [monoid_with_zero M] {f g : ℤ →*₀ M} (h_neg_one : ⇑f (-1) = ⇑g (-1)) (h_nat : f.comp int.of_nat_hom.to_monoid_with_zero_hom = g.comp int.of_nat_hom.to_monoid_with_zero_hom) :

f = g

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

theorem monoid_with_zero_hom.ext_int' {M : Type u_1} [monoid_with_zero M] {φ₁ φ₂ : ℤ →*₀ M} (h_neg_one : ⇑φ₁ (-1) = ⇑φ₂ (-1)) (h_pos : ∀ (n : ℕ), 0 < n → ⇑φ₁ ↑n = ⇑φ₂ ↑n) :

φ₁ = φ₂

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

@[simp]

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

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

f = int.cast_ring_hom α

@[simp]

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

⇑f ↑n = ↑n

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

f = g

@[protected, instance]

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

subsingleton (ℤ →+* R)

@[simp, norm_cast]

theorem int.cast_id (n : ℤ) :

↑n = n

@[simp]

theorem int.cast_ring_hom_int :

int.cast_ring_hom ℤ = ring_hom.id ℤ

theorem pi.int_apply {α : Type u_1} {β : Type u_2} [has_zero β] [has_one β] [has_add β] [has_neg β] (n : ℤ) (a : α) :

@[simp]

theorem pi.coe_int {α : Type u_1} {β : Type u_2} [has_zero β] [has_one β] [has_add β] [has_neg β] (n : ℤ) :

↑n = λ (_x : α), ↑n

@[simp, norm_cast]

theorem mul_opposite.op_int_cast {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] (z : ℤ) :

mul_opposite.op ↑z = ↑z

@[simp, norm_cast]

theorem mul_opposite.unop_int_cast {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] (n : ℤ) :

mul_opposite.unop ↑n = ↑n