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 #

Implementation note #

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

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

Coercion ℕ → ℤ as a ring_hom.

Equations
@[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
@[protected, instance]
def int.cast_coe {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :
Equations
@[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 : ) :
@[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 : ) :
@[simp, norm_cast]
theorem int.cast_neg_of_nat {α : Type u_1} [add_group α] [has_one α] (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
@[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.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 : ) :
@[simp, norm_cast]
theorem int.coe_nat_bit1 (n : ) :
@[simp, norm_cast]
theorem int.cast_bit0 {α : Type u_1} [ring α] (n : ) :
@[simp, norm_cast]
theorem int.cast_bit1 {α : Type u_1} [ring α] (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 α] :
@[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 : } :
theorem int.cast_nat_abs {R : Type u_1} [linear_ordered_ring R] (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 : ) :
@[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 : ) :
@[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) :
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
@[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]

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] {φ₁ φ₂ : monoid_with_zero_hom 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 : ) :
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
@[protected, instance]
@[simp, norm_cast]
theorem int.cast_id (n : ) :
n = n
theorem pi.int_apply {α : Type u_1} {β : Type u_2} [has_zero β] [has_one β] [has_add β] [has_neg β] (n : ) (a : α) :
n a = n
@[simp]
theorem pi.coe_int {α : Type u_1} {β : Type u_2} [has_zero β] [has_one β] [has_add β] [has_neg β] (n : ) :
n = λ (_x : α), n