Documentation

Init.Data.Int.Lemmas

Definitions of basic functions #

theorem Int.subNatNat_of_sub_eq_zero {m : Nat} {n : Nat} (h : n - m = 0) :
Int.subNatNat m n = (m - n)
theorem Int.subNatNat_of_sub_eq_succ {m : Nat} {n : Nat} {k : Nat} (h : n - m = k.succ) :
@[simp]
theorem Int.neg_zero :
-0 = 0
theorem Int.ofNat_add (n : Nat) (m : Nat) :
(n + m) = n + m
theorem Int.ofNat_mul (n : Nat) (m : Nat) :
(n * m) = n * m
theorem Int.ofNat_succ (n : Nat) :
n.succ = n + 1
theorem Int.neg_ofNat_succ (n : Nat) :
-n.succ = Int.negSucc n
theorem Int.neg_negSucc (n : Nat) :
-Int.negSucc n = n.succ
theorem Int.negSucc_coe (n : Nat) :
Int.negSucc n = -(n + 1)

These are only for internal use #

@[simp]
theorem Int.add_def {a : Int} {b : Int} :
a.add b = a + b
theorem Int.ofNat_add_ofNat (m : Nat) (n : Nat) :
m + n = (m + n)
theorem Int.ofNat_add_negSucc (m : Nat) (n : Nat) :
m + Int.negSucc n = Int.subNatNat m n.succ
theorem Int.negSucc_add_ofNat (m : Nat) (n : Nat) :
Int.negSucc m + n = Int.subNatNat n m.succ
@[simp]
theorem Int.mul_def {a : Int} {b : Int} :
a.mul b = a * b
theorem Int.ofNat_mul_ofNat (m : Nat) (n : Nat) :
m * n = (m * n)
theorem Int.ofNat_mul_negSucc' (m : Nat) (n : Nat) :
m * Int.negSucc n = Int.negOfNat (m * n.succ)
theorem Int.negSucc_mul_ofNat' (m : Nat) (n : Nat) :
Int.negSucc m * n = Int.negOfNat (m.succ * n)
theorem Int.negSucc_mul_negSucc' (m : Nat) (n : Nat) :
Int.negSucc m * Int.negSucc n = Int.ofNat (m.succ * n.succ)
theorem Int.ofNat_inj {m : Nat} {n : Nat} :
m = n m = n
theorem Int.ofNat_eq_zero {n : Nat} :
n = 0 n = 0
theorem Int.ofNat_ne_zero {n : Nat} :
n 0 n 0
theorem Int.negSucc_inj {m : Nat} {n : Nat} :
theorem Int.negSucc_eq (n : Nat) :
Int.negSucc n = -(n + 1)
@[simp]
@[simp]
@[simp]
@[simp]
theorem Int.neg_neg (a : Int) :
- -a = a
theorem Int.neg_inj {a : Int} {b : Int} :
-a = -b a = b
@[simp]
theorem Int.neg_eq_zero {a : Int} :
-a = 0 a = 0
theorem Int.neg_ne_zero {a : Int} :
-a 0 a 0
theorem Int.sub_eq_add_neg {a : Int} {b : Int} :
a - b = a + -b
theorem Int.add_neg_one (i : Int) :
i + -1 = i - 1
theorem Int.subNatNat_elim (m : Nat) (n : Nat) (motive : NatNatIntProp) (hp : ∀ (i n : Nat), motive (n + i) n i) (hn : ∀ (i m : Nat), motive m (m + i + 1) (Int.negSucc i)) :
motive m n (Int.subNatNat m n)
theorem Int.subNatNat_add_left {m : Nat} {n : Nat} :
Int.subNatNat (m + n) m = n
theorem Int.subNatNat_add_add (m : Nat) (n : Nat) (k : Nat) :
Int.subNatNat (m + k) (n + k) = Int.subNatNat m n
theorem Int.subNatNat_of_le {m : Nat} {n : Nat} (h : n m) :
Int.subNatNat m n = (m - n)
theorem Int.subNatNat_of_lt {m : Nat} {n : Nat} (h : m < n) :
Int.subNatNat m n = Int.negSucc (n - m).pred
theorem Int.add_comm (a : Int) (b : Int) :
a + b = b + a
instance Int.instCommutativeHAdd :
Std.Commutative fun (x1 x2 : Int) => x1 + x2
Equations
@[simp]
theorem Int.add_zero (a : Int) :
a + 0 = a
@[simp]
theorem Int.zero_add (a : Int) :
0 + a = a
theorem Int.ofNat_add_negSucc_of_lt {m : Nat} {n : Nat} (h : m < n.succ) :
theorem Int.subNatNat_sub {n : Nat} {m : Nat} (h : n m) (k : Nat) :
Int.subNatNat (m - n) k = Int.subNatNat m (k + n)
theorem Int.subNatNat_add (m : Nat) (n : Nat) (k : Nat) :
Int.subNatNat (m + n) k = m + Int.subNatNat n k
theorem Int.subNatNat_add_negSucc (m : Nat) (n : Nat) (k : Nat) :
theorem Int.add_assoc (a : Int) (b : Int) (c : Int) :
a + b + c = a + (b + c)
theorem Int.add_assoc.aux1 (m : Nat) (n : Nat) (c : Int) :
m + n + c = m + (n + c)
theorem Int.add_assoc.aux2 (m : Nat) (n : Nat) (k : Nat) :
instance Int.instAssociativeHAdd :
Std.Associative fun (x1 x2 : Int) => x1 + x2
Equations
theorem Int.add_left_comm (a : Int) (b : Int) (c : Int) :
a + (b + c) = b + (a + c)
theorem Int.add_right_comm (a : Int) (b : Int) (c : Int) :
a + b + c = a + c + b
theorem Int.add_left_neg (a : Int) :
-a + a = 0
theorem Int.add_right_neg (a : Int) :
a + -a = 0
@[simp]
theorem Int.neg_eq_of_add_eq_zero {a : Int} {b : Int} (h : a + b = 0) :
-a = b
theorem Int.eq_neg_of_eq_neg {a : Int} {b : Int} (h : a = -b) :
b = -a
theorem Int.eq_neg_comm {a : Int} {b : Int} :
a = -b b = -a
theorem Int.neg_eq_comm {a : Int} {b : Int} :
-a = b -b = a
theorem Int.neg_add_cancel_left (a : Int) (b : Int) :
-a + (a + b) = b
theorem Int.add_neg_cancel_left (a : Int) (b : Int) :
a + (-a + b) = b
theorem Int.add_neg_cancel_right (a : Int) (b : Int) :
a + b + -b = a
theorem Int.neg_add_cancel_right (a : Int) (b : Int) :
a + -b + b = a
theorem Int.add_left_cancel {a : Int} {b : Int} {c : Int} (h : a + b = a + c) :
b = c
theorem Int.neg_add {a : Int} {b : Int} :
-(a + b) = -a + -b
@[simp]
@[simp]
theorem Int.sub_self (a : Int) :
a - a = 0
@[simp]
theorem Int.sub_zero (a : Int) :
a - 0 = a
@[simp]
theorem Int.zero_sub (a : Int) :
0 - a = -a
theorem Int.sub_eq_zero_of_eq {a : Int} {b : Int} (h : a = b) :
a - b = 0
theorem Int.eq_of_sub_eq_zero {a : Int} {b : Int} (h : a - b = 0) :
a = b
theorem Int.sub_eq_zero {a : Int} {b : Int} :
a - b = 0 a = b
theorem Int.sub_sub (a : Int) (b : Int) (c : Int) :
a - b - c = a - (b + c)
theorem Int.neg_sub (a : Int) (b : Int) :
-(a - b) = b - a
theorem Int.sub_sub_self (a : Int) (b : Int) :
a - (a - b) = b
@[simp]
theorem Int.sub_neg (a : Int) (b : Int) :
a - -b = a + b
@[simp]
theorem Int.sub_add_cancel (a : Int) (b : Int) :
a - b + b = a
@[simp]
theorem Int.add_sub_cancel (a : Int) (b : Int) :
a + b - b = a
theorem Int.add_sub_assoc (a : Int) (b : Int) (c : Int) :
a + b - c = a + (b - c)
theorem Int.ofNat_sub {m : Nat} {n : Nat} (h : m n) :
(n - m) = n - m
theorem Int.negSucc_coe' (n : Nat) :
Int.negSucc n = -n - 1
theorem Int.subNatNat_eq_coe {m : Nat} {n : Nat} :
Int.subNatNat m n = m - n
theorem Int.toNat_sub (m : Nat) (n : Nat) :
(m - n).toNat = m - n
@[simp]
theorem Int.add_right_inj {i : Int} {j : Int} (k : Int) :
i + k = j + k i = j
@[simp]
theorem Int.add_left_inj {i : Int} {j : Int} (k : Int) :
k + i = k + j i = j
@[simp]
theorem Int.sub_left_inj {i : Int} {j : Int} (k : Int) :
k - i = k - j i = j
@[simp]
theorem Int.sub_right_inj {i : Int} {j : Int} (k : Int) :
i - k = j - k i = j
@[simp]
theorem Int.ofNat_mul_negSucc (m : Nat) (n : Nat) :
m * Int.negSucc n = -(m * n.succ)
@[simp]
theorem Int.negSucc_mul_ofNat (m : Nat) (n : Nat) :
Int.negSucc m * n = -(m.succ * n)
@[simp]
theorem Int.negSucc_mul_negSucc (m : Nat) (n : Nat) :
Int.negSucc m * Int.negSucc n = m.succ * n.succ
theorem Int.mul_comm (a : Int) (b : Int) :
a * b = b * a
instance Int.instCommutativeHMul :
Std.Commutative fun (x1 x2 : Int) => x1 * x2
Equations
theorem Int.ofNat_mul_negOfNat (m : Nat) (n : Nat) :
theorem Int.negOfNat_mul_ofNat (m : Nat) (n : Nat) :
theorem Int.mul_assoc (a : Int) (b : Int) (c : Int) :
a * b * c = a * (b * c)
instance Int.instAssociativeHMul :
Std.Associative fun (x1 x2 : Int) => x1 * x2
Equations
theorem Int.mul_left_comm (a : Int) (b : Int) (c : Int) :
a * (b * c) = b * (a * c)
theorem Int.mul_right_comm (a : Int) (b : Int) (c : Int) :
a * b * c = a * c * b
@[simp]
theorem Int.mul_zero (a : Int) :
a * 0 = 0
@[simp]
theorem Int.zero_mul (a : Int) :
0 * a = 0
theorem Int.ofNat_mul_subNatNat (m : Nat) (n : Nat) (k : Nat) :
m * Int.subNatNat n k = Int.subNatNat (m * n) (m * k)
theorem Int.negSucc_mul_subNatNat (m : Nat) (n : Nat) (k : Nat) :
Int.negSucc m * Int.subNatNat n k = Int.subNatNat (m.succ * k) (m.succ * n)
theorem Int.mul_add (a : Int) (b : Int) (c : Int) :
a * (b + c) = a * b + a * c
theorem Int.add_mul (a : Int) (b : Int) (c : Int) :
(a + b) * c = a * c + b * c
theorem Int.neg_mul_eq_neg_mul (a : Int) (b : Int) :
-(a * b) = -a * b
theorem Int.neg_mul_eq_mul_neg (a : Int) (b : Int) :
-(a * b) = a * -b
@[simp]
theorem Int.neg_mul (a : Int) (b : Int) :
-a * b = -(a * b)
@[simp]
theorem Int.mul_neg (a : Int) (b : Int) :
a * -b = -(a * b)
theorem Int.neg_mul_neg (a : Int) (b : Int) :
-a * -b = a * b
theorem Int.neg_mul_comm (a : Int) (b : Int) :
-a * b = a * -b
theorem Int.mul_sub (a : Int) (b : Int) (c : Int) :
a * (b - c) = a * b - a * c
theorem Int.sub_mul (a : Int) (b : Int) (c : Int) :
(a - b) * c = a * c - b * c
@[simp]
theorem Int.one_mul (a : Int) :
1 * a = a
@[simp]
theorem Int.mul_one (a : Int) :
a * 1 = a
theorem Int.mul_neg_one (a : Int) :
a * -1 = -a
theorem Int.neg_eq_neg_one_mul (a : Int) :
-a = -1 * a
theorem Int.mul_eq_zero {a : Int} {b : Int} :
a * b = 0 a = 0 b = 0
theorem Int.mul_ne_zero {a : Int} {b : Int} (a0 : a 0) (b0 : b 0) :
a * b 0
@[simp]
theorem Int.mul_ne_zero_iff {a : Int} {b : Int} :
a * b 0 a 0 b 0
theorem Int.eq_of_mul_eq_mul_right {a : Int} {b : Int} {c : Int} (ha : a 0) (h : b * a = c * a) :
b = c
theorem Int.eq_of_mul_eq_mul_left {a : Int} {b : Int} {c : Int} (ha : a 0) (h : a * b = a * c) :
b = c
theorem Int.mul_eq_mul_left_iff {a : Int} {b : Int} {c : Int} (h : c 0) :
c * a = c * b a = b
theorem Int.mul_eq_mul_right_iff {a : Int} {b : Int} {c : Int} (h : c 0) :
a * c = b * c a = b
theorem Int.eq_one_of_mul_eq_self_left {a : Int} {b : Int} (Hpos : a 0) (H : b * a = a) :
b = 1
theorem Int.eq_one_of_mul_eq_self_right {a : Int} {b : Int} (Hpos : b 0) (H : b * a = b) :
a = 1

NatCast lemmas

The following lemmas are later subsumed by e.g. Nat.cast_add and Nat.cast_mul in Mathlib but it is convenient to have these earlier, for users who only need Nat and Int.

theorem Int.natCast_zero :
0 = 0
theorem Int.natCast_one :
1 = 1
@[simp]
theorem Int.natCast_add (a : Nat) (b : Nat) :
(a + b) = a + b
@[simp]
theorem Int.natCast_mul (a : Nat) (b : Nat) :
(a * b) = a * b