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

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

@[simp]

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

↑0 = 0

source

ink

@[simp]

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

↑↑n = ↑n

source

ink

@[simp]

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

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

source

ink

@[simp]

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

↑1 = 1

source

ink

@[simp]

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

↑(-n) = -↑n

source

ink

@[simp]

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

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

source

ink

@[simp]

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

↑(Int.negOfNat n) = -↑n

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

theorem Int.ofNat_bit0 (n : ℕ) :

↑(bit0 n) = bit0 ↑n

source

ink

theorem Int.ofNat_bit1 (n : ℕ) :

↑(bit1 n) = bit1 ↑n

source

ink

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

↑(bit0 n) = bit0 ↑n

source

ink

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

↑(bit1 n) = bit1 ↑n

source

ink

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

↑2 = 2

source

ink

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

↑3 = 3

source

ink

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

↑4 = 4