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

@[simp]
theorem Nat.cast_sub {R : Type u} [AddGroupWithOne R] {m : } {n : } (h : m n) :
↑(n - m) = n - m
@[simp]
theorem Nat.cast_pred {R : Type u} [AddGroupWithOne R] {n : } :
0 < n↑(n - 1) = n - 1
@[simp]
theorem Int.cast_negSucc {R : Type u} [AddGroupWithOne R] (n : ) :
↑(Int.negSucc n) = -↑(n + 1)
@[simp]
theorem Int.cast_zero {R : Type u} [AddGroupWithOne R] :
0 = 0
@[simp]
theorem Int.cast_ofNat {R : Type u} [AddGroupWithOne R] (n : ) :
n = n
@[simp]
theorem Int.cast_one {R : Type u} [AddGroupWithOne R] :
1 = 1
@[simp]
theorem Int.cast_neg {R : Type u} [AddGroupWithOne R] (n : ) :
↑(-n) = -n
@[simp]
theorem Int.cast_subNatNat {R : Type u} [AddGroupWithOne R] (m : ) (n : ) :
↑(Int.subNatNat m n) = m - n
@[simp]
theorem Int.cast_negOfNat {R : Type u} [AddGroupWithOne R] (n : ) :
↑(Int.negOfNat n) = -n
@[simp]
theorem Int.cast_add {R : Type u} [AddGroupWithOne R] (m : ) (n : ) :
↑(m + n) = m + n
@[simp]
theorem Int.cast_sub {R : Type u} [AddGroupWithOne R] (m : ) (n : ) :
↑(m - n) = m - n
@[deprecated]
theorem Int.ofNat_bit0 (n : ) :
↑(bit0 n) = bit0 n
@[deprecated]
theorem Int.ofNat_bit1 (n : ) :
↑(bit1 n) = bit1 n
@[deprecated]
theorem Int.cast_bit0 {R : Type u} [AddGroupWithOne R] (n : ) :
↑(bit0 n) = bit0 n
@[deprecated]
theorem Int.cast_bit1 {R : Type u} [AddGroupWithOne R] (n : ) :
↑(bit1 n) = bit1 n
theorem Int.cast_two {R : Type u} [AddGroupWithOne R] :
2 = 2
theorem Int.cast_three {R : Type u} [AddGroupWithOne R] :
3 = 3
theorem Int.cast_four {R : Type u} [AddGroupWithOne R] :
4 = 4