Int.neg_add_cancel_right
theorem Int.neg_add_cancel_right : ∀ (a b : ℤ), a + -b + b = a
This theorem, `Int.neg_add_cancel_right`, states that for all integers `a` and `b`, if you add the negation of `b` to `a` and then add `b`, you will get back `a`. In mathematical notation, it asserts that ∀(a, b ∈ ℤ), a + (-b) + b = a. Essentially, this is a statement about the canceling property of addition with negation in the set of integers.
More concisely: For all integers `a` and `b`, `a + (-b) = a + b`. In other words, adding the negation of a number to a number is equivalent to not adding that number.
|
Int.mul_left_comm
theorem Int.mul_left_comm : ∀ (a b c : ℤ), a * (b * c) = b * (a * c)
This theorem, `Int.mul_left_comm`, states that for any three integers `a`, `b`, and `c`, the product of `a` and the product of `b` and `c` is equal to the product of `b` and the product of `a` and `c`. In mathematical terms, this would be written as $a \cdot (b \cdot c) = b \cdot (a \cdot c)$. This property is known as the left commutativity of multiplication over the integers.
More concisely: For any integers a, b, and c, a \* (b \* c) = (b \* a) \* c. (Left commutativity of multiplication over the integers)
|
Int.zero_mul
theorem Int.zero_mul : ∀ (a : ℤ), 0 * a = 0
This theorem states that for any integer 'a', the product of 0 and 'a' is always 0. It's a formal expression of the well-known mathematical rule that multiplying any number by zero results in zero.
More concisely: For all integers a, 0 * a = 0.
|
Int.sub_sub_self
theorem Int.sub_sub_self : ∀ (a b : ℤ), a - (a - b) = b
This theorem states that for all integers `a` and `b`, the result of subtracting `a - b` from `a` is always `b`. In other words, it's saying that if you take an integer `a`, subtract `b` from it, and then subtract this result from `a` again, you will always end up with `b`. In mathematical notation, this is expressed as `a - (a - b) = b` for all integers `a` and `b`.
More concisely: The theorem asserts that for all integers `a` and `b`, `a - (a - b) = b`.
|
Int.neg_mul_eq_neg_mul
theorem Int.neg_mul_eq_neg_mul : ∀ (a b : ℤ), -(a * b) = -a * b
This theorem states that for all integers `a` and `b`, the negation of the product of `a` and `b` is equal to the product of the negation of `a` and `b`. In other words, if we take any two integers, multiply them together, and then take the negation of the result, we will get the same value as if we had taken the negation of the first integer and then multiplied by the second integer. This theorem is a property of integer multiplication and follows from the well known fact that the multiplication of an integer by -1 results in the negation of the integer.
More concisely: For all integers `a` and `b`, the negation of `a * b` is equivalent to `(-a) * b` or `a * (-b)`.
|
Int.neg_zero
theorem Int.neg_zero : -0 = 0
This theorem states that the negation of zero in the integer number system is equal to zero. In other words, if you take zero and negate it, you still get zero. This holds true in the domain of all integers.
More concisely: The theorem asserts that the additive inverse of 0 in the integers equals 0.
|
Int.ofNat_succ
theorem Int.ofNat_succ : ∀ (n : ℕ), ↑n.succ = ↑n + 1
This theorem, `Int.ofNat_succ`, states that for all natural numbers `n`, the integer representation of the successor of `n` is equal to the integer representation of `n` plus 1. In other words, when you increment a natural number and then convert it to an integer, it's the same as if you had converted the number to an integer first and then added one. This theorem bridges the behavior of addition between natural numbers and integers in Lean 4.
More concisely: For all natural numbers `n`, `Int.ofNat (nat.succ n) = Int.ofNat n + 1`.
|
Int.sub_self
theorem Int.sub_self : ∀ (a : ℤ), a - a = 0
This theorem states that for any integer 'a', the result of subtracting 'a' from itself is always zero. In mathematical terms, it is expressing the property `a - a = 0` for all integers 'a'.
More concisely: For all integers 'a', the expression 'a - a' equals zero.
|
Int.neg_inj
theorem Int.neg_inj : ∀ {a b : ℤ}, -a = -b ↔ a = b
This theorem, `Int.neg_inj`, states that for all integers `a` and `b`, the negation of `a` is equal to the negation of `b` if and only if `a` is equal to `b`. In other words, this theorem asserts the injectivity of the negation operation on integers: distinct integers have distinct negations.
More concisely: For all integers `a` and `b`, if `~a = ~b` then `a = b`. (Negation of integers is injective.)
|
Int.mul_add
theorem Int.mul_add : ∀ (a b c : ℤ), a * (b + c) = a * b + a * c
This is the distributive property of multiplication over addition for integers. The theorem states that for all integers `a`, `b`, and `c`, the product of `a` and the sum of `b` and `c` is equal to the sum of the product of `a` and `b` and the product of `a` and `c`. In mathematical notation, this is expressed as `a * (b + c) = a * b + a * c`.
More concisely: The distributive property of multiplication over addition for integers states that for all integers `a`, `b`, and `c`, `a * (b + c)` equals `a * b + a * c`.
|
Int.mul_neg
theorem Int.mul_neg : ∀ (a b : ℤ), a * -b = -(a * b)
This theorem states that for all integer values `a` and `b`, the product of `a` and the negation of `b` (`-b`) is equal to the negation of the product of `a` and `b` (`-(a * b)`). In other words, multiplying an integer by another integer's negative is the same as negating the product of the two integers. This is consistent with the property of multiplication over the set of integers in mathematics.
More concisely: For all integers `a` and `b`, `a * -b` equals `- (a * b)`.
|
Int.subNatNat_eq_coe
theorem Int.subNatNat_eq_coe : ∀ {m n : ℕ}, Int.subNatNat m n = ↑m - ↑n
This theorem states that for all natural numbers `m` and `n`, the integer value obtained by the function `Int.subNatNat` applied to `m` and `n` is equivalent to the result of subtracting the integer equivalent of `n` from the integer equivalent of `m`. Here, the notation `↑m` and `↑n` denotes the integer equivalent of the natural numbers `m` and `n` respectively.
More concisely: For all natural numbers m and n, Int.subNatNat m n equals the integer value obtained by subtracting ↑n from ↑m.
|
Int.sub_add_cancel
theorem Int.sub_add_cancel : ∀ (a b : ℤ), a - b + b = a
This theorem states that for any two integers `a` and `b`, if you subtract `b` from `a` and then add `b` back, you get `a` back. In mathematical terms, it states that for all integers `a` and `b`, the equation `a - b + b = a` holds. This essentially captures the property of subtraction and addition being inverse operations.
More concisely: For all integers `a` and `b`, `a - b + b = a`.
|
Int.zero_add
theorem Int.zero_add : ∀ (a : ℤ), 0 + a = a
This theorem states that for any integer 'a', the result of adding 'a' to zero is 'a' itself, preserving the identity property of addition. In mathematical terms, it asserts that ∀ a ∈ ℤ, 0 + a = a.
More concisely: For all integers a, the addition of a to zero equals a. (i.e., 0 + a = a)
|
Int.add_left_cancel
theorem Int.add_left_cancel : ∀ {a b c : ℤ}, a + b = a + c → b = c
This theorem, `Int.add_left_cancel`, states that for any three integers `a`, `b`, and `c`, if the sum of `a` and `b` equals the sum of `a` and `c`, then `b` must be equal to `c`. In other words, in the context of integer addition, the addition of `a` can be cancelled from both sides of an equation without affecting the equality of `b` and `c`.
More concisely: If `a + b = a + c` in the context of integer addition, then `b = c`.
|
Int.add_neg_cancel_right
theorem Int.add_neg_cancel_right : ∀ (a b : ℤ), a + b + -b = a
This theorem states that for any two integers `a` and `b`, adding `b` and its negation `-b` to `a` will always result in `a`. In other words, the sum of an integer `a` and the addition of an integer `b` and its negation `-b` will always be `a`. This corresponds to the fact that adding any number with its additive inverse results in zero, hence does not change the value of `a`. In mathematical notation, this is expressed as `a + b + (-b) = a` for all `a`, `b` in the set of integers.
More concisely: For all integers `a` and `b`, the sum of `a`, `b`, and the negation of `b` equals `a`. In other words, `a + b + (-b) = a`.
|
Int.subNatNat_self
theorem Int.subNatNat_self : ∀ (n : ℕ), Int.subNatNat n n = 0
This theorem states that for any natural number `n`, the result of the function `Int.subNatNat` applied to `n` and `n` is always zero. In other words, subtracting a natural number from itself using the `Int.subNatNat` function always yields zero, regardless of the specific natural number being considered.
More concisely: For all natural numbers n, Int.subNatNat n n equals zero.
|
Int.add_sub_assoc
theorem Int.add_sub_assoc : ∀ (a b c : ℤ), a + b - c = a + (b - c)
This theorem, `Int.add_sub_assoc`, states that for all integers `a`, `b`, and `c`, the operation of adding `b` to `a` and then subtracting `c` is equivalent to adding `b - c` directly to `a`. In mathematical notation, this is expressed as `a + b - c = a + (b - c)`. In other words, it says that addition and subtraction of integers are associative operations.
More concisely: The theorem `Int.add_sub_assoc` asserts that for all integers `a`, `b`, and `c`, `a + (b - c)` is equal to `a + b - c`.
|
Int.subNatNat_of_lt
theorem Int.subNatNat_of_lt : ∀ {m n : ℕ}, m < n → Int.subNatNat m n = Int.negSucc (n - m).pred
This theorem, `Int.subNatNat_of_lt`, states that for every pair of natural numbers `m` and `n` where `m` is less than `n`, the subtraction of `m` from `n` in the domain of integers, as defined by the function `Int.subNatNat`, is equivalent to the negative of the successor of the predecessor of the difference of `n` and `m`. In other words, if `m` is less than `n`, subtracting `m` from `n` yields the negative of the successor of the result you get when you decrement `n - m` by 1. This is done using the natural numbers predecessor function `Nat.pred`. The theorem provides a specific case for the function `Int.subNatNat` when the first argument is smaller than the second one.
More concisely: For natural numbers `m` and `n` with `m < n`, `Int.subNatNat m n` equals the negative of the successor of `(n - m - 1)`.
|
Int.add_left_comm
theorem Int.add_left_comm : ∀ (a b c : ℤ), a + (b + c) = b + (a + c)
This theorem, `Int.add_left_comm`, states that for all integers `a`, `b`, and `c`, the operation of addition is left-commutative. In other words, adding `b` and `c` together and then adding `a` to the result is the same as adding `b` to the sum of `a` and `c`. This is expressed in mathematical notation as a + (b + c) = b + (a + c).
More concisely: For all integers `a`, `b`, and `c`, `a + (b + c) = b + (a + c)`.
|
Int.add_comm
theorem Int.add_comm : ∀ (a b : ℤ), a + b = b + a
This theorem, `Int.add_comm`, asserts the commutativity of addition for integers. Specifically, it states that for all integers `a` and `b`, the sum of `a` and `b` is equal to the sum of `b` and `a`. In mathematical notation, this would be expressed as ∀(a, b ∈ ℤ), a + b = b + a.
More concisely: For all integers `a` and `b`, `a + b` equals `b + a`.
|
Int.ofNat_mul_negSucc
theorem Int.ofNat_mul_negSucc : ∀ (m n : ℕ), ↑m * Int.negSucc n = -↑(m * n.succ)
This theorem states that for any two natural numbers `m` and `n`, the product of `m` and the successor of `n` with a negative sign is equal to the negation of the product of `m` and the successor of `n` when both are cast to integers. In other words, multiplying a natural number with the negative successor of another natural number in the integers is the same as taking the negative of the product of the two natural numbers, where the second one has been succeeded.
More concisely: For any natural numbers m and n, (-m * (Suc n)) = -(m * Suc n), where Suc denotes the successor function.
|
Int.mul_eq_zero
theorem Int.mul_eq_zero : ∀ {a b : ℤ}, a * b = 0 ↔ a = 0 ∨ b = 0
This theorem states that for any two integers `a` and `b`, the product `a * b` is equal to zero if and only if either `a` is zero or `b` is zero. This is a fundamental property of number systems, reflecting the fact that zero multiplied by any number results in zero.
More concisely: For any integers `a` and `b`, `a * b = 0` if and only if `a = 0` or `b = 0`.
|
Int.add_neg_cancel_left
theorem Int.add_neg_cancel_left : ∀ (a b : ℤ), a + (-a + b) = b
This theorem states that for any two integers `a` and `b`, if you add `a` to the sum of `-a` and `b`, you will get `b`. In more formal mathematical terms, this is expressing the property that adding the additive inverse of a number to that number results in zero, which when added to any other number, leaves that number unchanged. Thus, `a + (-a + b) = b` for all integers `a` and `b`.
More concisely: For all integers `a` and `b`, `a + (-a + b) = b`.
|
Int.ofNat_inj
theorem Int.ofNat_inj : ∀ {m n : ℕ}, ↑m = ↑n ↔ m = n
This theorem, `Int.ofNat_inj`, states that for any two natural numbers `m` and `n`, the assertion that the integer representation of `m` is equal to the integer representation of `n` is equivalent to the assertion that `m` is equal to `n`. In other words, coercing (or converting) natural numbers to integers preserves uniqueness. This is a statement about the injective property of the function that maps natural numbers to integers.
More concisely: The theorem `Int.ofNat_inj` asserts that for all natural numbers m and n, the equality of their integer representations implies the equality of m and n.
|
Int.ofNat_sub
theorem Int.ofNat_sub : ∀ {m n : ℕ}, m ≤ n → ↑(n - m) = ↑n - ↑m
This theorem states that for any two natural numbers 'm' and 'n', where 'm' is less than or equal to 'n', the integer produced by converting the difference 'n - m' into an integer is equal to the difference of the integers converted from 'n' and 'm'. In other words, the process of subtraction for natural numbers and their integer counterparts is consistent.
More concisely: For all natural numbers m and n with m <= n, (n - m) = int.of_nat (n.to_int) - int.of_nat (m.to_int).
|
Int.negSucc_mul_ofNat
theorem Int.negSucc_mul_ofNat : ∀ (m n : ℕ), Int.negSucc m * ↑n = -↑(m.succ * n)
This theorem states that for any natural numbers `m` and `n`, the product of the integer representation of the negative successor of `m` and the integer representation of `n` is equal to the negative of the integer representation of the product of the successor of `m` and `n`. In mathematical terms, this can be stated as: for all natural numbers `m` and `n`, `- (m+1) * n = - ((m+1) * n)`, where `m+1` is the successor of `m`.
More concisely: For all natural numbers `m` and `n`, the negative of the integer representation of `(m+1) * n` is equal to the integer representation of `-m * n`.
|
Int.negSucc_coe
theorem Int.negSucc_coe : ∀ (n : ℕ), Int.negSucc n = -↑(n + 1)
This theorem states that for every natural number `n`, the negative successor function on integers (`Int.negSucc`) applied to `n` is equal to the negation of the coersion (`↑`) of `n + 1` from a natural number to an integer. In simpler terms, it states that the negative successor of a natural number in the integer domain is the same as subtracting 1 from that number and making the result negative.
More concisely: For every natural number `n`, `Int.negSucc (n : Int) = -(nat.succ n)`.
|
Int.eq_of_mul_eq_mul_left
theorem Int.eq_of_mul_eq_mul_left : ∀ {a b c : ℤ}, a ≠ 0 → a * b = a * c → b = c
This theorem states that for any three integers `a`, `b`, and `c`, if `a` is not zero and the product of `a` and `b` is equal to the product of `a` and `c`, then `b` must be equal to `c`. In mathematical terms, this corresponds to the property of cancellation in the integers: if $ab = ac$ and $a \neq 0$, then $b = c$.
More concisely: If $a \neq 0$ and $ab = ac$, then $b = c$.
|
Int.mul_comm
theorem Int.mul_comm : ∀ (a b : ℤ), a * b = b * a
This theorem, `Int.mul_comm`, states that for all integers `a` and `b`, the multiplication of `a` and `b` is commutative. In other words, multiplying `a` by `b` is the same as multiplying `b` by `a`.
More concisely: For all integers `a` and `b`, `a * b` equals `b * a`.
|
Int.sub_zero
theorem Int.sub_zero : ∀ (a : ℤ), a - 0 = a
This theorem states that for any integer `a`, subtracting zero from `a` will result in `a`. In mathematical terms, it can be expressed as ∀a ∈ ℤ, a - 0 = a. It's a simple property of integers relating to the operation of subtraction.
More concisely: For all integers `a`, `a - 0 = a`.
|
Int.mul_one
theorem Int.mul_one : ∀ (a : ℤ), a * 1 = a
This theorem states that for every integer `a`, the product of `a` and 1 is `a`. In mathematical terms, this theorem represents the multiplicative identity property in the set of integers, which says that any number multiplied by 1 remains the same.
More concisely: For all integers a, a * 1 = a. (This statement asserts that the multiplicative identity 1 holds for integers.)
|
Int.negSucc_mul_negSucc
theorem Int.negSucc_mul_negSucc : ∀ (m n : ℕ), Int.negSucc m * Int.negSucc n = ↑m.succ * ↑n.succ
This theorem, `Int.negSucc_mul_negSucc`, states that for all natural numbers `m` and `n`, the product of the negated successors of `m` and `n` in the integers is equal to the product of the successors of `m` and `n` in the natural numbers. In mathematical terms, it means that if you take two natural numbers, increment them both, negate them and then multiply, you get the same result as if you had just incremented them and then multiplied.
More concisely: For all natural numbers m and n, (-(m+1) * (-(n+1)) = (m+1) * (n+1)).
|
Int.mul_zero
theorem Int.mul_zero : ∀ (a : ℤ), a * 0 = 0
This theorem states that for any integer `a`, the product of `a` and zero equals zero. In mathematical notation, it's expressed as ∀a ∈ ℤ, a * 0 = 0. This is a fundamental property of multiplication in the set of integers (ℤ), and it's an instance of the more general arithmetic property that any number multiplied by zero gives zero.
More concisely: For all integers `a`, `a` multiplied by zero equals zero. (Or more succinctly: For all `a` in ℤ, `a` * 0 = 0.)
|
Int.add_zero
theorem Int.add_zero : ∀ (a : ℤ), a + 0 = a
This theorem states that for every integer `a`, adding zero to `a` results in `a`. In mathematical terms, it expresses the identity property of addition for integers, i.e., `a + 0 = a` for all integers `a`.
More concisely: The theorem asserts that for all integers `a`, `a + 0 = a`.
|
Int.neg_mul
theorem Int.neg_mul : ∀ (a b : ℤ), -a * b = -(a * b)
This theorem, `Int.neg_mul`, states that for any two integers `a` and `b`, the result of multiplying negative `a` (`-a`) with `b` is the same as the negative of the product of `a` and `b` (`-(a * b)`). This is essentially a restatement of the rule in arithmetic that multiplying a negative number by a positive number yields a negative number.
More concisely: For any integers `a` and `b`, `-(a * b) = (-a) * b`.
|
Int.ofNat_ne_zero
theorem Int.ofNat_ne_zero : ∀ {n : ℕ}, ↑n ≠ 0 ↔ n ≠ 0
This theorem states that for any natural number `n`, the integer representation of `n` (denoted as `↑n`) is not equal to zero if and only if `n` itself is not equal to zero. In other words, a natural number and its integer equivalent share the same zero-nonzero status.
More concisely: For any natural number `n`, the integer `↑n` is non-zero if and only if `n` is non-zero.
|
Int.ofNat_add
theorem Int.ofNat_add : ∀ (n m : ℕ), ↑(n + m) = ↑n + ↑m
This theorem states that for any two natural numbers `n` and `m`, the operation of adding the numbers and then converting the result to an integer is equivalent to converting each number to an integer first and then adding them. In other words, if you have two natural numbers, `n` and `m`, then the integer representation of `(n + m)` is equal to the sum of the integer representation of `n` and the integer representation of `m`. In mathematical notation, we could write this as: "For all natural numbers `n` and `m`, `↑(n + m) = ↑n + ↑m`." In this equation, the `↑` symbol is used to denote the conversion from a natural number to an integer.
More concisely: For all natural numbers `n` and `m`, the conversion of `(n + m)` to an integer is equal to the sum of the conversions of `n` and `m` to integers. (i.e., `↑(n + m) = ↑n + ↑m`)
|
Int.neg_neg
theorem Int.neg_neg : ∀ (a : ℤ), - -a = a
This theorem states that for every integer 'a', the double negation of 'a' equals 'a'. In other words, if you take the negation of the negation of any integer, you get the original integer. This is a fundamental property of integer numbers and is commonly known in mathematics.
More concisely: For all integers a, ∠∠a = a, where ∠ denotes negation. (This is also known as "de Morgan's law for integers" or "double negation elimination" for integers.)
|
Int.neg_add_cancel_left
theorem Int.neg_add_cancel_left : ∀ (a b : ℤ), -a + (a + b) = b
This theorem, `Int.neg_add_cancel_left`, states that for all integers `a` and `b`, the sum of the negation of `a` and the sum of `a` and `b` is equal to `b`. In mathematical terms, it's saying that for all integers $a$ and $b$, $-a + (a + b) = b$. This aligns with the principle that adding a number and its negation results in zero, effectively canceling each other out.
More concisely: For all integers `a` and `b`, the negation of `a` plus the sum of `a` and `b` equals `b`. In mathematical notation, $-a + (a + b) = b$.
|
Int.one_mul
theorem Int.one_mul : ∀ (a : ℤ), 1 * a = a
This theorem states that for any integer 'a', the product of 1 and 'a' is equal to 'a'. In other words, it confirms the multiplicative identity property in the set of integers, which says that any number multiplied by 1 remains unchanged.
More concisely: For all integers a, 1 * a = a. (This statement asserts the multiplicative identity property in the integers.)
|
Int.natCast_add
theorem Int.natCast_add : ∀ (a b : ℕ), ↑(a + b) = ↑a + ↑b
This theorem states that for any two natural numbers `a` and `b`, the casting of their sum to an integer is equal to the sum of these two numbers individually cast to integers. In other words, casting to an integer preserves the operation of addition from natural numbers. This is symbolically expressed as `(a + b) = a + b` for two natural numbers `a` and `b`, where the operations and equality are interpreted in the domain of integers.
More concisely: The theorem asserts that the casting of natural numbers `a` and `b` to integers and their subsequent addition is equal to the individual casting and addition of `a` and `b` as integers. Symbolically, `(to_int a + to_int b) = to_int (a + b)`.
|
Int.sub_sub
theorem Int.sub_sub : ∀ (a b c : ℤ), a - b - c = a - (b + c)
This theorem, `Int.sub_sub`, states a property about subtraction for all integers. Specifically, it says that for any three integers `a`, `b`, and `c`, subtracting `b` and then `c` from `a` is the same as subtracting the sum of `b` and `c` from `a`. In other words, `a - b - c` equals `a - (b + c)` for all integer values of `a`, `b`, and `c`.
More concisely: For all integers `a`, `b`, and `c`, `a - b - c` equals `a - (b + c)`.
|
Int.add_assoc
theorem Int.add_assoc : ∀ (a b c : ℤ), a + b + c = a + (b + c)
This theorem, `Int.add_assoc`, states that for all integers `a`, `b`, and `c`, the operation of addition is associative. In other words, for any integers `a`, `b`, and `c`, the sum of `a`, `b`, and `c` remains the same regardless of how the numbers are grouped. This is written formally in mathematics as `a + b + c = a + (b + c)`.
More concisely: The theorem `Int.add_assoc` asserts that for all integers `a`, `b`, and `c`, the association of addition is valid, that is, `(a + b) + c = a + (b + c)`.
|
Int.subNatNat_of_le
theorem Int.subNatNat_of_le : ∀ {m n : ℕ}, n ≤ m → Int.subNatNat m n = ↑(m - n)
This theorem, `Int.subNatNat_of_le`, states that for any two natural numbers `m` and `n`, if `n` is less than or equal to `m`, then the result of the function `Int.subNatNat` applied to `m` and `n` is equal to the pure integer (using the coercion `↑`) of the difference between `m` and `n`. In other words, when `n` is less than or equal to `m`, subtracting `n` from `m` in the `Int.subNatNat` function behaves just like normal subtraction in natural numbers.
More concisely: For all natural numbers `m` and `n`, if `n ≤ m`, then `Int.subNatNat m n = ↑(m - n)`.
|
Int.subNatNat_elim
theorem Int.subNatNat_elim :
∀ (m n : ℕ) (motive : ℕ → ℕ → ℤ → Prop),
(∀ (i n : ℕ), motive (n + i) n ↑i) →
(∀ (i m : ℕ), motive m (m + i + 1) (Int.negSucc i)) → motive m n (Int.subNatNat m n)
This theorem, `Int.subNatNat_elim`, is a principle of elimination for the subtraction of two natural numbers. It takes four arguments: two natural numbers `m` and `n`, and a property `motive` which relates two natural numbers to an integer. The theorem then states that if this property holds for every pair of natural numbers `(n + i, n)` and their difference `i`, and for every pair of natural numbers `(m, m + i + 1)` and the negative of the successor of `i`, then it must also hold for the pair `(m, n)` and their difference as computed by `Int.subNatNat`. Essentially, this theorem asserts that if we can prove certain facts about differences of natural numbers and their negatives, we can generalize these facts to all natural numbers.
More concisely: If for all natural numbers `i`, the property `motive` holds for `(n + i, n)` and `i`, and for `(m, m + i + 1)` and `-(i + 1)`, then `motive` holds for `(m, n)` and `Int.subNatNat m n`.
|
Int.negSucc_eq
theorem Int.negSucc_eq : ∀ (n : ℕ), Int.negSucc n = -(↑n + 1)
This theorem, `Int.negSucc_eq`, states that for any natural number `n`, the function `Int.negSucc n` is equivalent to the negation of the sum of the natural number `n` and one. In mathematical terms, this can be written as `Int.negSucc n = -(n + 1)`, where `n` is a natural number.
More concisely: The theorem `Int.negSucc_eq` asserts that `Int.negSucc n = -(n + 1)` for all natural numbers `n`.
|
Int.neg_mul_neg
theorem Int.neg_mul_neg : ∀ (a b : ℤ), -a * -b = a * b
This theorem states that for all integers `a` and `b`, the product of the negations of `a` and `b` (i.e., `-a * -b`) is equal to the product of `a` and `b` (i.e., `a * b`). This is a formal expression of the mathematical rule that the product of two negative numbers is a positive number.
More concisely: For all integers a and b, the product of the negations of a and b equals the product of a and b. That is, -a * -b = a * b.
|
Int.add_mul
theorem Int.add_mul : ∀ (a b c : ℤ), (a + b) * c = a * c + b * c
This theorem, `Int.add_mul`, states that for any three integers `a`, `b`, and `c`, the operation of adding `a` and `b` together and then multiplying the result by `c` is equal to the operation of multiplying `a` by `c` and `b` by `c` separately and then adding those results together. In mathematical terms, this theorem is expressing the distributive property of multiplication over addition for integers, `(a + b) * c = a * c + b * c`.
More concisely: The theorem asserts that for all integers a, b, and c, (a + b) * c = a * c + b * c.
|
Int.add_sub_cancel
theorem Int.add_sub_cancel : ∀ (a b : ℤ), a + b - b = a
This theorem, `Int.add_sub_cancel`, states that for any two integers `a` and `b`, if you add `b` to `a` and then subtract `b`, you will get back `a`. In mathematical terms, it expresses the property \(a + b - b = a\) for all integers \(a\) and \(b\). This is a basic property of addition and subtraction in the set of integers, reflecting the cancellation law of addition/subtraction.
More concisely: For all integers `a` and `b`, `a + b = a + (-b)`.
|
Int.ofNat_mul
theorem Int.ofNat_mul : ∀ (n m : ℕ), ↑(n * m) = ↑n * ↑m
This theorem, `Int.ofNat_mul`, demonstrates a property of the multiplication operation involving natural numbers and integers. Specifically, it states that for all natural numbers `n` and `m`, the result of first multiplying `n` and `m` (as natural numbers) and then casting the result to an integer is the same as first casting `n` and `m` to integers and then multiplying them. In mathematical notation, this can be written as \( \forall n, m \in \mathbb{N}, \, \text{Int}(n \cdot m) = \text{Int}(n) \cdot \text{Int}(m) \). This theorem exemplifies the preservation of the multiplication operation under the embedding of the natural numbers into the integers.
More concisely: For all natural numbers `n` and `m`, the conversion of `n` and `m` to integers and their multiplication is equal to the multiplication of the integer conversions of `n` and `m`. In mathematical notation, \( \forall n, m \in \mathbb{N}, \ \text{Int}(n) \cdot \text{Int}(m) = \text{Int}(n \cdot m) \).
|
Int.add_right_neg
theorem Int.add_right_neg : ∀ (a : ℤ), a + -a = 0
This theorem, `Int.add_right_neg`, states that for any integer `a`, adding the negation of `a` to `a` results in zero. In mathematical terms, it asserts that for all integers `a`, the equation `a + (-a) = 0` holds. In other words, it's expressing the property that any number plus its negative counterpart equals zero, a fundamental property of addition in the set of integers.
More concisely: For all integers `a`, `a + (-a) = 0`.
|
Int.mul_sub
theorem Int.mul_sub : ∀ (a b c : ℤ), a * (b - c) = a * b - a * c
This theorem states that for all integers `a`, `b`, and `c`, the result of `a` multiplied by the difference of `b` and `c` is equal to the result of `a` multiplied by `b` minus `a` multiplied by `c`. In mathematical notation, this can be written as: for all $a$, $b$, $c$ in $\mathbb{Z}$, $a \cdot (b - c) = a \cdot b - a \cdot c$. This theorem essentially confirms the distribution law of multiplication over subtraction for integers.
More concisely: For all integers `a`, `b`, and `c`, `a` *(b - c)* equals `a` *`b`* `-` `a` *`c`*.
|
Int.mul_assoc
theorem Int.mul_assoc : ∀ (a b c : ℤ), a * b * c = a * (b * c)
This theorem states that for all integers `a`, `b`, and `c`, the operation of multiplication is associative. That is, the result of first multiplying `a` and `b` and then multiplying the result by `c` is the same as the result of first multiplying `b` and `c` and then multiplying `a` by that result. In mathematical notation, this is expressed as `a * b * c = a * (b * c)`.
More concisely: The theorem asserts that for all integers `a`, `b`, and `c`, the associativity of multiplication holds: `a * (b * c) = (a * b) * c`.
|
Int.neg_mul_eq_mul_neg
theorem Int.neg_mul_eq_mul_neg : ∀ (a b : ℤ), -(a * b) = a * -b
This theorem states that for any two integers `a` and `b`, the negative of their product is equal to the product of `a` and the negative of `b`. In other words, if you multiply two numbers and then take the negative of the result, it's the same as if you had multiplied the first number by the negative of the second number. This theorem encapsulates a fundamental property of integer multiplication.
More concisely: For all integers a and b, (-1) * (a * b) = a * (-b).
|
Int.sub_eq_zero_of_eq
theorem Int.sub_eq_zero_of_eq : ∀ {a b : ℤ}, a = b → a - b = 0
The theorem `Int.sub_eq_zero_of_eq` states that for any two integers `a` and `b`, if `a` equals `b`, then the result of subtracting `b` from `a` is `0`. In mathematical terms, this theorem asserts that for all integers `a` and `b`, if `a = b`, then `a - b = 0`.
More concisely: For all integers `a` and `b`, if `a = b`, then `a - b = 0`.
|
Int.neg_add
theorem Int.neg_add : ∀ {a b : ℤ}, -(a + b) = -a + -b
This theorem, `Int.neg_add`, states that for all integers `a` and `b`, the negation of the sum of `a` and `b` is equal to the sum of the negations of `a` and `b`. In other words, given any two integers, the negative of their sum is the same as the sum of their negatives. This is essentially a formal way of stating the distributive property of negation over addition for integers.
More concisely: For all integers `a` and `b`, `-(a + b) = a + (-b)`.
|
Int.add_left_neg
theorem Int.add_left_neg : ∀ (a : ℤ), -a + a = 0
This theorem, `Int.add_left_neg`, states that for any integer `a`, the sum of `-a` (the negation of `a`) and `a` equals 0. In other words, when you add an integer and its negative counterpart, you always get zero. This is a formal restatement of a fundamental property of integers in Lean 4.
More concisely: For any integer `a`, `-a + a = 0`.
|
Int.zero_sub
theorem Int.zero_sub : ∀ (a : ℤ), 0 - a = -a
This theorem, `Int.zero_sub`, states that for any integer `a`, the result of subtracting `a` from zero (`0 - a`) is equal to the negative of `a` (`-a`). This follows the algebraic rule that 0 minus a given number is equivalent to the negative of that number.
More concisely: For any integer `a`, `0 - a` equals `-a`.
|
Int.sub_eq_add_neg
theorem Int.sub_eq_add_neg : ∀ {a b : ℤ}, a - b = a + -b
This theorem states that for any two integers `a` and `b`, the operation of subtracting `b` from `a` is equivalent to the operation of adding the additive inverse of `b` to `a`. In other words, `a - b` is the same as `a + -b`. This is a fundamental property of integer arithmetic and can be extended to any ring, not just the integers.
More concisely: For all integers `a` and `b`, `a - b` is equal to `a + (-b)`.
|