Documentation

Mathlib.Data.Int.Cast.Basic

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 Mathlib.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 Mathlib.Data.Int.Cast.Defs is Mathlib.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_ite {R : Type u} [IntCast R] (P : Prop) [Decidable P] (m n : ℤ) :
↑(if P then m else n) = if P then ↑m else ↑n
source
@[simp]
theorem Int.cast_negSucc {R : Type u} [AddGroupWithOne R] (n : ℕ) :
↑(negSucc n) = -↑(n + 1)
source
@[simp]
theorem Int.cast_zero {R : Type u} [AddGroupWithOne R] :
↑0 = 0
source
@[simp]
theorem Int.cast_natCast {R : Type u} [AddGroupWithOne R] (n : ℕ) :
↑↑n = ↑n
source
@[simp]
theorem Int.cast_ofNat {R : Type u} [AddGroupWithOne R] (n : ℕ) [n.AtLeastTwo] :
↑(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 : ℕ) :
↑(subNatNat m n) = ↑m - ↑n
source
@[simp]
theorem Int.cast_negOfNat {R : Type u} [AddGroupWithOne R] (n : ℕ) :
↑(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
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
source
@[simp]
theorem zsmul_one {R : Type u_1} [AddGroupWithOne R] (n : ℤ) :
n • 1 = ↑n