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) : Int.subNatNat m n = Int.negSucc k

@[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_zero : -↑0 = 0

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)

theorem Int.negOfNat_eq {n : Nat} : Int.negOfNat n = -Int.ofNat n

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

theorem Int.negSucc_add_negSucc (m : Nat) (n : Nat) : Int.negSucc m + Int.negSucc n = Int.negSucc (m + n).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} : Int.negSucc m = Int.negSucc n ↔ m = n

theorem Int.negSucc_eq (n : Nat) : Int.negSucc n = -(↑n + 1)

@[simp]

theorem Int.negSucc_ne_zero (n : Nat) : Int.negSucc n ≠ 0

@[simp]

theorem Int.zero_ne_negSucc (n : Nat) : 0 ≠ Int.negSucc n

@[simp]

theorem Int.Nat.cast_ofNat_Int {n : Nat} : ↑(OfNat.ofNat n) = OfNat.ofNat n

@[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 : Nat → Nat → Int → Prop) (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_right {m : Nat} {n : Nat} : Int.subNatNat m (m + n + 1) = Int.negSucc 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

• Int.instCommutativeHAdd = ⋯

@[simp]

theorem Int.add_zero (a : Int) : a + 0 = a

@[simp]

theorem Int.zero_add (a : Int) : 0 + a = a

instance Int.instLawfulIdentityHAddOfNat : Std.LawfulIdentity (fun (x1 x2 : Int) => x1 + x2) 0

Equations

• Int.instLawfulIdentityHAddOfNat = ⋯

theorem Int.ofNat_add_negSucc_of_lt {m : Nat} {n : Nat} (h : m < n.succ) : Int.ofNat m + Int.negSucc n = Int.negSucc (n - m)

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) : Int.subNatNat m n + Int.negSucc k = Int.subNatNat m (n + k.succ)

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) : Int.negSucc m + Int.negSucc n + ↑k = Int.negSucc m + (Int.negSucc n + ↑k)

instance Int.instAssociativeHAdd : Std.Associative fun (x1 x2 : Int) => x1 + x2

Equations

• Int.instAssociativeHAdd = ⋯

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.subNatNat_self (n : Nat) : Int.subNatNat n n = 0

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]

theorem Int.negSucc_sub_one (n : Nat) : Int.negSucc n - 1 = Int.negSucc (n + 1)

@[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

• Int.instCommutativeHMul = ⋯

theorem Int.ofNat_mul_negOfNat (m : Nat) (n : Nat) : ↑m * Int.negOfNat n = Int.negOfNat (m * n)

theorem Int.negOfNat_mul_ofNat (m : Nat) (n : Nat) : Int.negOfNat m * ↑n = Int.negOfNat (m * n)

theorem Int.negSucc_mul_negOfNat (m : Nat) (n : Nat) : Int.negSucc m * Int.negOfNat n = Int.ofNat (m.succ * n)

theorem Int.negOfNat_mul_negSucc (m : Nat) (n : Nat) : Int.negOfNat n * Int.negSucc m = Int.ofNat (n * m.succ)

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

• Int.instAssociativeHMul = ⋯

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.negOfNat_eq_subNatNat_zero (n : Nat) : Int.negOfNat n = Int.subNatNat 0 n

theorem Int.ofNat_mul_subNatNat (m : Nat) (n : Nat) (k : Nat) : ↑m * Int.subNatNat n k = Int.subNatNat (m * n) (m * k)

theorem Int.negOfNat_add (m : Nat) (n : Nat) : Int.negOfNat m + Int.negOfNat n = Int.negOfNat (m + n)

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

instance Int.instLawfulIdentityHMulOfNat : Std.LawfulIdentity (fun (x1 x2 : Int) => x1 * x2) 1

Equations

• Int.instLawfulIdentityHMulOfNat = ⋯

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