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_natCast {R : Type u} [AddGroupWithOne R] (n : ) :
n = n
@[simp]
theorem Int.cast_ofNat {R : Type u} [AddGroupWithOne R] (n : ) [n.AtLeastTwo] :
@[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
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