Cast of integers (additional theorems) #

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]

theorem Nat.cast_sub {R : Type u} [AddGroupWithOne R] {m : ℕ} {n : ℕ} (h : m ≤ n) :

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

source

@[simp]

theorem Nat.cast_pred {R : Type u} [AddGroupWithOne R] {n : ℕ} :

0 < n → ↑(n - 1) = ↑n - 1

source

@[simp]

theorem Int.cast_negSucc {R : Type u} [AddGroupWithOne R] (n : ℕ) :

↑(Int.negSucc n) = -↑(n + 1)

source

@[simp]

theorem Int.cast_zero {R : Type u} [AddGroupWithOne R] :

↑0 = 0

source

@[simp]

theorem Int.cast_ofNat {R : Type u} [AddGroupWithOne R] (n : ℕ) :

↑↑n = ↑n

source

@[simp]

theorem Int.int_cast_ofNat {R : Type u} [AddGroupWithOne R] (n : ℕ) [Nat.AtLeastTwo n] :

↑(OfNat.ofNat n) = OfNat.ofNat n

source

@[simp]

theorem Int.cast_one {R : Type u} [AddGroupWithOne R] :

↑1 = 1

source

@[simp]

theorem Int.cast_neg {R : Type u} [AddGroupWithOne R] (n : ℤ) :

↑(-n) = -↑n

source

@[simp]

theorem Int.cast_subNatNat {R : Type u} [AddGroupWithOne R] (m : ℕ) (n : ℕ) :

↑(Int.subNatNat m n) = ↑m - ↑n

source

@[simp]

theorem Int.cast_negOfNat {R : Type u} [AddGroupWithOne R] (n : ℕ) :

↑(Int.negOfNat n) = -↑n

source

@[simp]

theorem Int.cast_add {R : Type u} [AddGroupWithOne R] (m : ℤ) (n : ℤ) :

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

source

@[simp]

theorem Int.cast_sub {R : Type u} [AddGroupWithOne R] (m : ℤ) (n : ℤ) :

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

source

@[deprecated]

theorem Int.ofNat_bit0 (n : ℕ) :

↑(bit0 n) = bit0 ↑n

source

@[deprecated]

theorem Int.ofNat_bit1 (n : ℕ) :

↑(bit1 n) = bit1 ↑n

source

@[deprecated]

theorem Int.cast_bit0 {R : Type u} [AddGroupWithOne R] (n : ℤ) :

↑(bit0 n) = bit0 ↑n

source

@[deprecated]

theorem Int.cast_bit1 {R : Type u} [AddGroupWithOne R] (n : ℤ) :

↑(bit1 n) = bit1 ↑n

source

theorem Int.cast_two {R : Type u} [AddGroupWithOne R] :

↑2 = 2

source

theorem Int.cast_three {R : Type u} [AddGroupWithOne R] :

↑3 = 3

source

theorem Int.cast_four {R : Type u} [AddGroupWithOne R] :

↑4 = 4