mathlib3 documentation

data.int.cast.basic

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).

There is also data.int.cast.lemmas, which includes lemmas stated in terms of algebraic homomorphisms, and results involving the order structure of ℤ.

By contrast, this file's only import beyond data.int.cast.defs is algebra.group.basic.

source
@[simp, norm_cast]
theorem nat.cast_sub {R : Type u} [add_group_with_one R] {m n : ℕ} (h : m ≤ n) :
↑(n - m) = ↑n - ↑m
source
@[simp, norm_cast]
theorem nat.cast_pred {R : Type u} [add_group_with_one R] {n : ℕ} :
0 < n → ↑(n - 1) = ↑n - 1
source
@[simp]
theorem int.cast_neg_succ_of_nat {R : Type u} [add_group_with_one R] (n : ℕ) :
↑-[1+ n] = -↑(n + 1)
source
@[simp, norm_cast]
theorem int.cast_zero {R : Type u} [add_group_with_one R] :
↑0 = 0
source
@[simp, norm_cast]
theorem int.cast_coe_nat {R : Type u} [add_group_with_one R] (n : ℕ) :
↑↑n = ↑n
source
@[simp, norm_cast]
theorem int.cast_one {R : Type u} [add_group_with_one R] :
↑1 = 1
source
@[simp, norm_cast]
theorem int.cast_neg {R : Type u} [add_group_with_one R] (n : ℤ) :
↑-n = -↑n
source
@[simp]
theorem int.cast_sub_nat_nat {R : Type u} [add_group_with_one R] (m n : ℕ) :
↑(int.sub_nat_nat m n) = ↑m - ↑n
source
theorem int.neg_of_nat_eq (n : ℕ) :
int.neg_of_nat n = -↑n
source
@[simp]
theorem int.cast_neg_of_nat {R : Type u} [add_group_with_one R] (n : ℕ) :
↑(int.neg_of_nat n) = -↑n
source
@[simp, norm_cast]
theorem int.cast_add {R : Type u} [add_group_with_one R] (m n : ℤ) :
↑(m + n) = ↑m + ↑n
source
@[simp, norm_cast]
theorem int.cast_sub {R : Type u} [add_group_with_one R] (m n : ℤ) :
↑(m - n) = ↑m - ↑n
source
@[simp, norm_cast]
theorem int.coe_nat_bit0 (n : ℕ) :
↑(bit0 n) = bit0 ↑n
source
@[simp, norm_cast]
theorem int.coe_nat_bit1 (n : ℕ) :
↑(bit1 n) = bit1 ↑n
source
@[simp, norm_cast]
theorem int.cast_bit0 {R : Type u} [add_group_with_one R] (n : ℤ) :
↑(bit0 n) = bit0 ↑n
source
@[simp, norm_cast]
theorem int.cast_bit1 {R : Type u} [add_group_with_one R] (n : ℤ) :
↑(bit1 n) = bit1 ↑n
source
theorem int.cast_two {R : Type u} [add_group_with_one R] :
↑2 = 2
source
theorem int.cast_three {R : Type u} [add_group_with_one R] :
↑3 = 3
source
theorem int.cast_four {R : Type u} [add_group_with_one R] :
↑4 = 4