Int.emod_add_emod
theorem Int.emod_add_emod : ∀ (m n k : ℤ), (m % n + k) % n = (m + k) % n
This theorem states that for any three integers `m`, `n`, and `k`, the remainder of the sum `(m % n + k)` when divided by `n` is equal to the remainder of the sum `(m + k)` when divided by `n`. In other words, adding `k` either before or after taking the modulus does not change the final result. This is a property of the modular arithmetic in integer domain.
More concisely: For any integers `m`, `n`, and `k`, `(m % n + k) % n = (m + k) % n`.
|
Int.natAbs_dvd_natAbs
theorem Int.natAbs_dvd_natAbs : ∀ {a b : ℤ}, a.natAbs ∣ b.natAbs ↔ a ∣ b
This theorem is stating a relationship between the absolute values of integers and the divisibility of those integers. More specifically, for any two integers `a` and `b`, the absolute value of `a` divides the absolute value of `b` if and only if `a` divides `b`. This means that the concept of divisibility is preserved when taking the absolute values of the integers.
More concisely: For all integers a and b, |a| |b| if and only if a | b. (Where "|" represents the absolute value and "|/" represents divisibility.)
|
Int.mul_ediv_cancel_left
theorem Int.mul_ediv_cancel_left : ∀ {a : ℤ} (b : ℤ), a ≠ 0 → a * b / a = b
This theorem states that for all integer values `a` and `b`, as long as `a` is not zero, the result of multiplying `a` and `b` and then dividing by `a` is equal to `b`. This is a representation of the fundamental property of division, where multiplying a number by another number and then dividing it by the original number should yield the multiplied number, assuming the divisor is not zero.
More concisely: For all integers `a` and `b` with `a ≠ 0`, `(a * b) / a = b`.
|
Int.ediv_mul_cancel
theorem Int.ediv_mul_cancel : ∀ {a b : ℤ}, b ∣ a → a / b * b = a
This theorem states that for any two integers `a` and `b`, if `b` divides `a` (i.e., `a` is divisible by `b` without remainder), then the result of `a` divided by `b` and subsequent multiplication by `b` equals to `a`. In other words, the division and subsequent multiplication effectively cancel out provided `b` divides `a` without leaving a remainder.
More concisely: If `a` is divisible by `b`, then `a = (a / b) * b`.
|
Int.mul_ediv_assoc
theorem Int.mul_ediv_assoc : ∀ (a : ℤ) {b c : ℤ}, c ∣ b → a * b / c = a * (b / c)
This theorem is about the relationship between integer division and multiplication in the context of divisibility. It states that for any integers `a`, `b`, and `c`, if `c` divides `b` (denoted as `c ∣ b`), then the integer division of `a * b` by `c` is equal to `a` multiplied by the integer division of `b` by `c`. In mathematical notation, this would be expressed as: if `c` divides `b`, then `(a * b) / c = a * (b / c)`. This theorem, therefore, illustrates an important property of integer division when it involves divisible numbers.
More concisely: If `c` divides `b`, then `(a * b) / c = a * (b / c)` for any integers `a`, `b`, and `c`.
|
Int.add_mul_emod_self_left
theorem Int.add_mul_emod_self_left : ∀ (a b c : ℤ), (a + b * c) % b = a % b
This theorem states that for any three integers `a`, `b`, and `c`, the remainder of the division of `(a + b * c)` by `b` is equal to the remainder of the division of `a` by `b`. In other words, adding `b * c` to `a` does not change the remainder of `a` when divided by `b`. This can be expressed mathematically as `(a + b * c) mod b = a mod b`.
More concisely: The theorem asserts that for any integers `a`, `b`, and `c`, `(a + b * c) % b = a % b`, where "%" denotes remainder.
|
Int.ediv_zero
theorem Int.ediv_zero : ∀ (a : ℤ), a / 0 = 0
This theorem states that for any integer `a`, the integer division of `a` by zero is equal to zero. In the context of Lean 4, the `/` operator represents integer division. Note that while in many contexts, division by zero is undefined, in Lean 4, it is defined to be zero for all integers.
More concisely: For all integers `a`, the result of the integer division of `a` by zero is equal to zero.
|
Int.emod_def
theorem Int.emod_def : ∀ (a b : ℤ), a % b = a - b * (a / b)
This theorem states that for all integer values `a` and `b`, the modulus operation `a % b` is equivalent to the operation `a - b * (a / b)`. In other words, the remainder of the division of `a` by `b` is the same as `a` minus the product of `b` and the integer quotient of `a` divided by `b`.
More concisely: For all integers `a` and `b`, `a % b` equals `a - b * (a \ dividedBy b)`. (In mathematical notation: `a % b = a - b * (a \ div b)`)
|
Int.ediv_eq_zero_of_lt
theorem Int.ediv_eq_zero_of_lt : ∀ {a b : ℤ}, 0 ≤ a → a < b → a / b = 0
This theorem states that for any two integers `a` and `b`, if `a` is non-negative and less than `b`, then the integer division of `a` by `b` equals zero. In mathematical terms, for all `a` and `b` in the set of integers such that `0 ≤ a < b`, we have `a / b = 0`. This follows from the definition of integer division where the quotient is rounded towards zero.
More concisely: For all integers `a` and `b` with `0 ≤ a < b`, we have `a / b = 0`.
|
Int.add_emod
theorem Int.add_emod : ∀ (a b n : ℤ), (a + b) % n = (a % n + b % n) % n
This theorem states that for all integers `a`, `b`, and `n`, the remainder of the sum of `a` and `b` after division by `n` is the same as the remainder of the sum of the remainders of `a` and `b` after division by `n`. In mathematical terms, this can be represented as `(a + b) mod n = (a mod n + b mod n) mod n`.
More concisely: The theorem asserts that for all integers `a`, `b`, and `n`, `(a + b) % n = (a % n + b % n) % n`.
|
Int.mul_emod_right
theorem Int.mul_emod_right : ∀ (a b : ℤ), a * b % a = 0
This theorem states that for all integer values `a` and `b`, the remainder of the product `a * b` divided by `a` is always 0. In other words, `a * b` is always a multiple of `a` for any pair of integers `a` and `b`. This is an application of the property of divisibility in integer multiplication.
More concisely: For all integers `a` and `b`, `a * b` is a multiple of `a`.
|
Int.add_mul_emod_self
theorem Int.add_mul_emod_self : ∀ {a b c : ℤ}, (a + b * c) % c = a % c
This theorem states that for any three integers `a`, `b`, and `c`, the modulo of the sum of `a` and the product of `b` and `c` with `c` is equal to the modulo of `a` with `c`. In mathematical notation, this can be written as `(a + b * c) mod c = a mod c`.
More concisely: For any integers `a`, `b`, and `c`, `(a + b * c) % c = a % c`.
|
Int.dvd_of_emod_eq_zero
theorem Int.dvd_of_emod_eq_zero : ∀ {a b : ℤ}, b % a = 0 → a ∣ b
This theorem states that for any two integers `a` and `b`, if the remainder of `b` divided by `a` (`b % a`) is zero, then `a` divides `b` (`a ∣ b`). In other words, it says that if `b` is a multiple of `a` such that there is no remainder when `b` is divided by `a`, then `a` is a divisor of `b`.
More concisely: If `a` divides `b` in the integer ring, then the remainder of `b` divided by `a` is zero. (In other words, `a ∣ b` implies `b % a = 0`.)
|
Int.emod_add_cancel_right
theorem Int.emod_add_cancel_right : ∀ {m n k : ℤ} (i : ℤ), (m + i) % n = (k + i) % n ↔ m % n = k % n
This theorem states that for all integers `m`, `n`, `k`, and `i`, the equivalence of the remainders of `m + i` and `k + i` when divided by `n` implies the equivalence of the remainders of `m` and `k` when divided by `n`. In other words, if `(m + i) mod n` equals `(k + i) mod n`, then `m mod n` equals `k mod n`. This theorem essentially asserts that the addition of a same integer `i` to two numbers `m` and `k` doesn't affect the congruence relation of `m` and `k` mod `n`.
More concisely: If `m` is congruent to `k` modulo `n`, then `(m + i)` is congruent to `(k + i)` modulo `n` for any integer `i`.
|
Int.mul_fdiv_cancel
theorem Int.mul_fdiv_cancel : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → (a * b).fdiv b = a
This theorem states that for any integer `a` and any non-zero integer `b`, when you perform floor division (`Int.fdiv`) of the product of `a` and `b` by `b`, the result is `a`. Essentially, it's stating that if you multiply an integer by another integer and then do floor division by the second integer, you get the first integer back.
More concisely: For any integers `a` and `b` (`b` non-zero), `a * Int.div b = a * Quot.↑ (b : Int)`. (Here, `Int.div` denotes integer division and `Quot.↑` denotes the up-conversion of rational quotients to integers.)
|
Int.ediv_one
theorem Int.ediv_one : ∀ (a : ℤ), a / 1 = a
This theorem states that for any integer 'a', dividing 'a' by 1 is equal to 'a' itself. In other words, it proves the well-known mathematical fact that when any number is divided by 1, the quotient is the number itself.
More concisely: For any integer 'a', 'a' divided by 1 equals 'a' itself.
|
Int.ofNat_dvd_left
theorem Int.ofNat_dvd_left : ∀ {n : ℕ} {z : ℤ}, ↑n ∣ z ↔ n ∣ z.natAbs
This theorem, `Int.ofNat_dvd_left`, states that for any natural number `n` and any integer `z`, the integer representation of `n` (denoted by `↑n`) divides `z` if and only if `n` divides the absolute value (the natural number equivalent) of `z`. In other words, the divisibility relationship between a natural number and an integer is equivalent to the divisibility relationship between the same natural number and the absolute value of the integer.
More concisely: For any natural number n and integer z, n divides z if and only if n divides the absolute value of z.
|
Int.ofNat_dvd
theorem Int.ofNat_dvd : ∀ {m n : ℕ}, ↑m ∣ ↑n ↔ m ∣ n
This theorem states that for any two natural numbers `m` and `n`, `m` divides `n` if and only if the integer representation of `m` divides the integer representation of `n`. Here, `↑m` and `↑n` denote the integer representations of the natural numbers `m` and `n`, respectively. The `∀` symbol denotes universality, meaning that the statement holds for all instances of `m` and `n`. The `∣` symbol represents the divides relation.
More concisely: For any natural numbers m and n, m divides n if and only if their respective integer representations have the relation that one is a multiple of the other.
|
Int.zero_emod
theorem Int.zero_emod : ∀ (b : ℤ), 0 % b = 0
This theorem states that for any integer `b`, the remainder when zero is divided by `b` is always zero. In mathematical terms, it expresses that for all integers `b`, the modulo operation `0 mod b` equals zero.
More concisely: For all integers `b`, `0 mod b` equals zero.
|
Int.add_ediv_of_dvd_right
theorem Int.add_ediv_of_dvd_right : ∀ {a b c : ℤ}, c ∣ b → (a + b) / c = a / c + b / c
This theorem states that for any three integers `a`, `b`, and `c`, if `c` divides `b` (in mathematical terms, this would be written as `c | b`), then the expression `(a + b) / c` is equal to the sum of the individual divisions `a / c + b / c`. This essentially expresses a distributive property of integer division where the divisor `c` divides one of the dividends (`b` in this case).
More concisely: If `c` divides `b`, then `(a + b) / c` equals the sum `a / c + b / c`.
|
Int.natAbs_dvd
theorem Int.natAbs_dvd : ∀ {a b : ℤ}, ↑a.natAbs ∣ b ↔ a ∣ b
The theorem `Int.natAbs_dvd` states that for any two integers `a` and `b`, the absolute value of `a` (in natural numbers) divides `b` if and only if `a` divides `b`. In other words, the divisibility relationship between `a` and `b` is maintained even when we replace `a` with its absolute value.
More concisely: For integers `a` and `b`, `|a|` divides `b` if and only if `a` divides `b`.
|
Int.dvd_sub_of_emod_eq
theorem Int.dvd_sub_of_emod_eq : ∀ {a b c : ℤ}, a % b = c → b ∣ a - c
This theorem states that for any three integers `a`, `b`, and `c`, if the remainder of `a` divided by `b` is equal to `c`, then `b` divides the difference between `a` and `c`. In mathematical terms, this theorem asserts that if `a % b = c`, then `b` is a divisor of `a - c`.
More concisely: If `a` is congruent to `c` modulo `b`, then `b` is a divisor of `a - c`. (Or equivalently, `a - c` is a multiple of `b`.)
|
Int.ediv_neg
theorem Int.ediv_neg : ∀ (a b : ℤ), a / -b = -(a / b)
This theorem states that for any two integers `a` and `b`, the floor division of `a` by `-b` is equal to the negation of the floor division of `a` by `b`. In other words, dividing an integer by a negative integer is the same as negating the result of dividing that integer by the positive counterpart of the negative integer. This is the standard behavior in mathematics where division by a negative number results in a negative quotient.
More concisely: For all integers `a` and `b`, `floor a (-b) = neg (floor a b)`.
|
Int.emod_eq_of_lt
theorem Int.emod_eq_of_lt : ∀ {a b : ℤ}, 0 ≤ a → a < b → a % b = a
This theorem states that for any two integers `a` and `b`, if `a` is non-negative and less than `b`, then the remainder of `a` divided by `b` is `a` itself. In other words, if you have an integer `a` that is at least zero and less than an integer `b`, when you divide `a` by `b`, the remainder will be `a`. This is a property of the modulo operation.
More concisely: For any integers `a` and `b` with `a` non-negative and less than `b`, `a` % `b` equals `a`.
|
Int.ediv_mul_le
theorem Int.ediv_mul_le : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → a / b * b ≤ a
This theorem states that for all integers `a` and non-zero integer `b`, the result of integer division of `a` by `b` when multiplied by `b` is less than or equal to `a`. Intuitively, this is because integer division truncates any remainder, so multiplying the quotient by the divisor will not exceed the original dividend.
More concisely: For all integers a and non-zero b, the result of their integer division a ∕ b satisfies a ≤ (a ∕ b) * b.
|
Int.mul_ediv_cancel
theorem Int.mul_ediv_cancel : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → a * b / b = a
This theorem states that for any integer `a` and any non-zero integer `b`, the product of `a` and `b` divided by `b` equals `a`. In other words, when you multiply an integer by another integer and then divide the result by the same integer you multiplied with (which is not zero), you get back the original integer. This is a foundational property related to the cancellation law of multiplication and division in integer arithmetic.
More concisely: For any integers `a` and `b` with `b ≠ 0`, we have `(a * b) / b = a`.
|
Int.zero_div
theorem Int.zero_div : ∀ (b : ℤ), Int.div 0 b = 0
This theorem states that for any integer `b`, the integer division of zero by `b` equals zero. In mathematical terms, it's saying that ∀b ∈ ℤ, 0 ÷ b = 0.
More concisely: For all integers `b`, the quotient of zero by `b` is equal to zero.
|
Int.add_emod_self
theorem Int.add_emod_self : ∀ {a b : ℤ}, (a + b) % b = a % b
This theorem states that for any two integers `a` and `b`, the remainder of the sum of `a` and `b` divided by `b` is the same as the remainder of `a` divided by `b`. In mathematical notation, this theorem is expressed as `(a + b) mod b = a mod b`. It is a property of modulo operations in the set of integers.
More concisely: For any integers `a` and `b`, the remainder of `a + b` when divided by `b` equals the remainder of `a` when divided by `b`. In other words, `(a + b) % b = a % b`.
|
Int.emod_zero
theorem Int.emod_zero : ∀ (a : ℤ), a % 0 = a
This theorem states that for any integer `a`, the remainder of `a` divided by zero is `a` itself. In other words, the modulus operation `%` when applied with zero as the divisor returns the original integer `a`.
More concisely: For any integer `a`, `a % 0 = a`.
|
Int.fmod_eq_emod
theorem Int.fmod_eq_emod : ∀ (a : ℤ) {b : ℤ}, 0 ≤ b → a.fmod b = a % b
This theorem states that for all integers `a` and `b`, if `b` is non-negative (i.e., `b` is greater than or equal to zero), then the flooring modulus of `a` and `b` (`Int.fmod a b`) is equal to the standard modulus of `a` and `b` (`a % b`). In other words, when the divisor is non-negative, the result of the flooring division-based modulus operation is the same as the result of the standard modulus operation in Lean.
More concisely: For all integers `a` and `b` with `b` non-negative, `Int.fmod a b` equals `a % b`.
|
Int.dvd_trans
theorem Int.dvd_trans : ∀ {a b c : ℤ}, a ∣ b → b ∣ c → a ∣ c
This theorem states that for any three integers `a`, `b`, and `c`, if `a` divides `b` and `b` divides `c`, then `a` also divides `c`. In other words, the "divides" relation is transitive on the integers: it can pass from `a` to `b` and from `b` to `c`, hence from `a` to `c`. This theorem is a form of the transitive property applied to integer division.
More concisely: If `a` divides `b` and `b` divides `c`, then `a` divides `c`. (Transitivity of integer division)
|
Int.add_emod_self_left
theorem Int.add_emod_self_left : ∀ {a b : ℤ}, (a + b) % a = b % a
This theorem states that for any two integers `a` and `b`, the result of adding `b` to `a` and then taking the modulus of this sum with respect to `a` is equal to the result of taking the modulus of `b` with respect to `a`. In mathematical terms, it says that `(a + b) mod a` is equal to `b mod a` for all integers `a` and `b`.
More concisely: For all integers `a` and `b`, `(a + b) % a` equals `b % a`. Here, `%` denotes the modulo operation.
|
Int.mul_div_cancel_left
theorem Int.mul_div_cancel_left : ∀ {a : ℤ} (b : ℤ), a ≠ 0 → (a * b).div a = b
This theorem states that for any two integers 'a' and 'b', where 'a' is not zero, the integer division of the product of 'a' and 'b' by 'a' is equal to 'b'. This is essentially a property of integer multiplication and division that mirrors the cancellation law in algebra.
More concisely: For any non-zero integer 'a' and integer 'b', the quotient of their product by 'a' equals 'b'.
|
Int.emod_lt_of_pos
theorem Int.emod_lt_of_pos : ∀ (a : ℤ) {b : ℤ}, 0 < b → a % b < b
This theorem states that for any integer `a` and any positive integer `b`, the remainder (`a % b`) of the division of `a` by `b` is always less than `b`. This is a commonly identified property of the modulus operation in number theory.
More concisely: For all integers `a` and positive integers `b`, `a % b` is less than `b`.
|
Int.emod_emod
theorem Int.emod_emod : ∀ (a b : ℤ), a % b % b = a % b
This theorem states that for any two integers 'a' and 'b', the modulus of 'a' with respect to 'b', taken modulus 'b' again, is equal to the modulus of 'a' with respect to 'b'. In other words, if you take the remainder of 'a' divided by 'b', and then find the remainder of that result divided by 'b' again, you'll just get the remainder of 'a' divided by 'b'. Mathematically, this can be represented as: `(a mod b) mod b = a mod b`.
More concisely: For any integers 'a' and 'b', the repeated application of the modulo operation, i.e., `(a mod b) mod b`, is equal to `a mod b`.
|
Int.dvd_natAbs
theorem Int.dvd_natAbs : ∀ {a b : ℤ}, a ∣ ↑b.natAbs ↔ a ∣ b
This theorem states that for any two integers `a` and `b`, `a` divides the absolute value of `b` if and only if `a` divides `b`. In other words, it asserts that the divisibility of an integer `a` by another integer `b` is equivalent to the divisibility of `a` by the absolute value of `b`. Here, the notation `a ∣ b` means "a divides b", and `↑(Int.natAbs b)` represents the absolute value of `b`.
More concisely: For any integers `a` and `b`, `a` divides `b` if and only if `a` divides the absolute value of `b`. In symbols, `a ∣ b <-> a ∣ ↑(Int.natAbs b)`.
|
Int.div_zero
theorem Int.div_zero : ∀ (a : ℤ), a.div 0 = 0
This theorem in the Lean 4 language states that for any integer `a`, when `a` is divided by 0, the result is 0. In mathematical terms, this can be written as: ∀a ∈ ℤ, a/0 = 0.
More concisely: For all integers `a`, `a/0 = 0`.
|
Int.fmod_def
theorem Int.fmod_def : ∀ (a b : ℤ), a.fmod b = a - b * a.fdiv b
This theorem defines the integer modulus operation (`Int.fmod`) in terms of integer division (`Int.fdiv`). For any two integers `a` and `b`, the remainder of the division of `a` by `b` (as computed by `Int.fmod a b`) is equal to the difference of `a` and the product of `b` and the floor of the division of `a` by `b` (computed as `b * Int.fdiv a b`). In mathematical terms, it expresses the fact that `a mod b = a - ⌊a/b⌋ * b`.
More concisely: For any integers `a` and `b`, `a % b = a - floor(a / b) * b`, where `%` denotes the modulo operation.
|
Int.zero_ediv
theorem Int.zero_ediv : ∀ (b : ℤ), 0 / b = 0
This theorem states that for any integer `b`, the integer division of `0` by `b` equals `0`. In other words, if you divide zero by any integer, the result is always zero.
More concisely: For all integers b, 0 divided by b equals 0.
|
Int.mul_ediv_mul_of_pos
theorem Int.mul_ediv_mul_of_pos : ∀ {a : ℤ} (b c : ℤ), 0 < a → a * b / (a * c) = b / c
This theorem states that for all integers `a`, `b`, and `c`, if `a` is greater than zero, then the integer division of the product of `a` and `b` by the product of `a` and `c` equals the integer division of `b` by `c`. In mathematical terms, if $a > 0$, then $\frac{a \cdot b}{a \cdot c} = \frac{b}{c}$. This theorem is a particular case of cancelling factors in a fraction, specifically when dealing with integer division and positive integers.
More concisely: For all integers a, b, and c where a > 0, the integer quotient of a * b by a * c equals the integer quotient of b by c.
|
Int.dvd_neg
theorem Int.dvd_neg : ∀ {a b : ℤ}, a ∣ -b ↔ a ∣ b
This theorem states that for all integers `a` and `b`, `a` divides `-b` if and only if `a` divides `b`. In other words, the divisibility relationship between two integers is not affected by the sign of the dividend. This is because, in integer arithmetic, a number is considered to divide another number if there is an integer quotient such that the product of the divisor and the quotient equals the dividend. Changing the sign of the dividend simply changes the sign of the quotient, but does not affect the fundamental divisibility relationship.
More concisely: For all integers `a` and `b`, `a` divides `b` if and only if `a` divides `-b`.
|
Int.div_eq_of_eq_mul_right
theorem Int.div_eq_of_eq_mul_right : ∀ {a b c : ℤ}, b ≠ 0 → a = b * c → a.div b = c
This theorem states that for any three integers `a`, `b`, and `c`, if `b` is not equal to zero and `a` is equal to the product of `b` and `c`, then the integer division of `a` by `b` is equal to `c`. Essentially, it is saying that if you have an equation of the form `a = b * c`, where `b` is not zero, you can divide both sides by `b` to get `c = a div b`.
More concisely: If integers `a`, `b`, and `c` satisfy `b ≠ 0` and `a = b * c`, then `a / b = c`.
|
Int.mul_emod
theorem Int.mul_emod : ∀ (a b n : ℤ), a * b % n = a % n * (b % n) % n
This theorem states that for any three integers `a`, `b`, and `n`, the remainder of the product of `a` and `b` when divided by `n` is equal to the product of the remainders of `a` and `b` when divided by `n`, which itself is then divided by `n`. In mathematical notation, this is expressing the identity `a * b mod n = ((a mod n) * (b mod n)) mod n`.
More concisely: The theorem asserts that for any integers `a`, `b`, and `n`, the remainder of their product taken modulo `n` equals the remainder of their individual products taken modulo `n`, also modulo `n`. In other words, `(a * b) mod n = (a mod n) * (b mod n) mod n`.
|
Int.emod_eq_emod_iff_emod_sub_eq_zero
theorem Int.emod_eq_emod_iff_emod_sub_eq_zero : ∀ {m n k : ℤ}, m % n = k % n ↔ (m - k) % n = 0
This theorem states that for any three integers `m`, `n`, and `k`, `m` modulo `n` equals `k` modulo `n` if and only if the modulus of the difference of `m` and `k` with respect to `n` equals zero. In mathematical notation, this theorem says that for all integers m, n, and k, m mod n = k mod n if and only if (m - k) mod n = 0.
More concisely: For integers m, n, and k, m congruent to k modulo n if and only if (m - k) is a multiple of n. (Or using the mathematical notation: m ≡ k (mod n) if and only if (m - k) is in the congruence class of 0 modulo n.)
|
Int.mod_def
theorem Int.mod_def : ∀ (a b : ℤ), a.mod b = a - b * a.div b
This theorem describes the definition of the modulus operation on integers in Lean. For any two integers `a` and `b`, the result of `Int.mod a b` is defined as the difference of `a` and the product of `b` with the integer division of `a` by `b`, denoted as `b * Int.div a b`. In mathematical terms, this can be expressed as `a mod b = a - b*(a div b)`.
More concisely: The modulus operation of two integers `a` and `b` is equivalent to the difference of `a` and the product of `b` and the quotient of `a` by `b`. In Lean, this is expressed as `a mod b = a - b * (a / b)`.
|
Int.mod_add_div
theorem Int.mod_add_div : ∀ (a b : ℤ), a.mod b + b * a.div b = a
This theorem states that for any two integers `a` and `b`, the sum of the modulus of `a` with respect to `b` and the product of `b` and the integer division of `a` by `b` is equal to `a`. In mathematical terms, it's equivalent to the equation `(a mod b) + b * (a div b) = a` for all integer `a` and `b`. This property is a fundamental aspect of the division algorithm in number theory.
More concisely: For all integers `a` and `b`, the theorem asserts that `(a % b) + b * (a / b) = a`, where `%` denotes modulus and `/` denotes integer division.
|
Int.div_one
theorem Int.div_one : ∀ (a : ℤ), a.div 1 = a
This theorem states that for any integer `a`, the result of integer division of `a` by `1` is `a` itself. In mathematical terms, it asserts that for all integers `a`, `a ÷ 1 = a`. This is because any number divided by one stays the same.
More concisely: For all integers `a`, `a` divided by `1` equals `a`. (Or, more concisely: `∀ a: ℤ, a / 1 = a`)
|
Int.le_ediv_of_mul_le
theorem Int.le_ediv_of_mul_le : ∀ {a b c : ℤ}, 0 < c → a * c ≤ b → a ≤ b / c
This theorem states that for any three integers `a`, `b`, and `c`, if `c` is greater than 0 and the product of `a` and `c` is less than or equal to `b`, then `a` is less than or equal to the integral division of `b` by `c`. In mathematical terms, if $c > 0$, $a \cdot c \leq b$, then $a \leq \lfloor \frac{b}{c} \rfloor$.
More concisely: If `c` is a positive integer and `a * c` is less than or equal to `b`, then `a` is less than or equal to the integer quotient of `b` by `c`. (Or, mathematically: If $c > 0$ and $a \cdot c \leq b$, then $a \leq \lfloor \frac{b}{c} \rfloor$.)
|
Int.mul_div_cancel
theorem Int.mul_div_cancel : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → (a * b).div b = a
This theorem states that for any integer `a` and any non-zero integer `b`, if you multiply `a` by `b` and then divide the result by `b`, you get `a` back. In essence, it captures the behavior of division undoing multiplication in the integers, under the condition that we are not dividing by zero. This is expressed in LaTeX as: ∀a, b ∈ ℤ, b ≠ 0 → (a * b) ÷ b = a.
More concisely: For any integer `a` and non-zero integer `b`, `a * b / b` equals `a`.
|
Int.fdiv_eq_ediv
theorem Int.fdiv_eq_ediv : ∀ (a : ℤ) {b : ℤ}, 0 ≤ b → a.fdiv b = a / b
This theorem states that for any integer `a` and any non-negative integer `b`, the floored division of `a` by `b` (denoted as `Int.fdiv a b` in Lean 4) is equal to the Euclidean division of `a` by `b` (denoted as `a / b` in Lean 4). Basically, this is saying that when you are dividing an integer by a non-negative integer, the concept of floored division aligns with that of Euclidean division.
More concisely: For any integer `a` and non-negative integer `b`, `Int.fdiv a b` equals the quotient and remainder of the Euclidean division of `a` by `b`.
|
Int.div_neg
theorem Int.div_neg : ∀ (a b : ℤ), a.div (-b) = -a.div b
This theorem states that for all integers `a` and `b`, the integer division of `a` by the negation of `b` is equal to the negation of the integer division of `a` by `b`. In mathematical terms, for every pair of integers `(a, b)`, we have that `a ÷ (-b) = -(a ÷ b)`. This theorem establishes a property of integer division concerning division by negative numbers.
More concisely: For all integers `a` and `b`, `a / (-b) = -(a / b)`.
|
Int.ediv_add_emod
theorem Int.ediv_add_emod : ∀ (a b : ℤ), b * (a / b) + a % b = a
This theorem states that for any two integers `a` and `b`, the product of `b` and the integer division of `a` by `b`, when added to the modulus of `a` with respect to `b`, equals `a`. This is the mathematical version of the formal statement that the division with remainder of an integer `a` by another integer `b` can be recombined to yield the original `a`, i.e., `a = b * (a div b) + (a mod b)`.
More concisely: For any integers `a` and `b`, `a = b * (a // b) + a % b`.
|
Int.dvd_sub
theorem Int.dvd_sub : ∀ {a b c : ℤ}, a ∣ b → a ∣ c → a ∣ b - c
This theorem states that for any three integers `a`, `b`, and `c`, if `a` divides `b` and `a` also divides `c`, then `a` divides the difference `b - c`. This is a property of divisibility in the set of integers. In mathematical notation, this would be written as: if $a|b$ and $a|c$, then $a|(b-c)$.
More concisely: If `a` divides `b` and `c`, then `a` divides the difference `b - c` (in the set of integers). Alternatively, mathematically: if $a|b$ and $a|c$, then $a|(b-c)$.
|
Int.neg_div
theorem Int.neg_div : ∀ (a b : ℤ), (-a).div b = -a.div b
This theorem states that for all integer pairs `a` and `b`, the integer division of `-a` by `b` is equal to the negation of the integer division of `a` by `b`. In other words, negating `a` before division by `b` is the same as negating the result of the division of `a` by `b`. This holds for all integers `a` and `b` with mathematical notation as: ∀ a, b ∈ ℤ, (-a) ÷ b = -(a ÷ b).
More concisely: For all integers `a` and `b`, the negative of the integer division of `a` by `b` is equal to the integer division of the negated `a` by `b`. In mathematical notation: ∀ a, b ∈ ℤ, -(a ÷ b) = (-\_ a) ÷ b.
|
Int.mul_ediv_self_le
theorem Int.mul_ediv_self_le : ∀ {x k : ℤ}, k ≠ 0 → k * (x / k) ≤ x
This theorem states that for any integers `x` and `k`, with `k` not equal to 0, the product of `k` and the integer division of `x` by `k` is less than or equal to `x`. In other words, k times the floor division of x by k never exceeds x itself. This is a property of how integer (floor) division works, where the quotient is always less than or equal to the original value when multiplied by the divisor.
More concisely: For all integers x and k (with k != 0), k * ⌊x / k⌋ ≤ x.
|
Int.emod_nonneg
theorem Int.emod_nonneg : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → 0 ≤ a % b
This theorem states that for any integer `a` and any non-zero integer `b`, the modulus of `a` with respect to `b` (`a % b`) is always greater than or equal to 0. In other words, when `a` is divided by `b`, the remainder (which is what the modulus operation calculates) is never negative. This is a standard property of the modulus operation in mathematics.
More concisely: For all integers `a` and non-zero `b`, `a % b` is a non-negative integer.
|
Int.mul_div_cancel'
theorem Int.mul_div_cancel' : ∀ {a b : ℤ}, a ∣ b → a * b.div a = b
This theorem states that for any two integers `a` and `b`, if `a` divides `b` then multiplying `a` by the result of dividing `b` by `a` gives us back `b`. In other words, `a * (b / a) = b` when `a` is a divisor of `b`. It's a specific case of a property about integer division, showing that the normal cancellation law holds when the divisor is a factor of the dividend.
More concisely: For integers `a` and `b`, if `a` divides `b`, then `a * (b / a) = b`.
|
Int.add_mul_ediv_right
theorem Int.add_mul_ediv_right : ∀ (a b : ℤ) {c : ℤ}, c ≠ 0 → (a + b * c) / c = a / c + b
This theorem states that for any integers `a`, `b`, and `c` (where `c` is not zero), the operation of dividing the sum of `a` and the product of `b` and `c` by `c` is equal to the sum of the division of `a` by `c` and `b`. In mathematical terms, it's expressing the property `(a + b * c) / c = a / c + b` in the ring of integers.
More concisely: The theorem asserts that for any integers `a`, `b`, and non-zero `c`, the quotient of the sum of `a` and the product of `b` and `c` by `c` equals the sum of the quotient of `a` by `c` and `b`. In other words, `(a + b * c) / c = a / c + b`.
|
Int.lt_mul_ediv_self_add
theorem Int.lt_mul_ediv_self_add : ∀ {x k : ℤ}, 0 < k → x < k * (x / k) + k
This theorem states that for any integers `x` and `k`, where `k` is greater than 0, `x` is less than `k` times the quotient of `x` divided by `k`, plus `k`. In mathematical terms, this can be written as `x < k * (x / k) + k` for all integers `x` and `k` where `k > 0`.
More concisely: For all integers `x` and `k` with `k > 0`, `x` is less than `k` times the quotient of `x` by `k` plus `k`. Equivalently, `x < k * (x / k) + k`.
|
Int.dvd_iff_emod_eq_zero
theorem Int.dvd_iff_emod_eq_zero : ∀ (a b : ℤ), a ∣ b ↔ b % a = 0
This theorem states that for any two integers `a` and `b`, `a` divides `b` if and only if the remainder of `b` divided by `a` equals zero. This is a reciprocal relationship, meaning that if `a` divides `b` then `b` modulus `a` will be zero, and conversely, if `b` modulus `a` equals zero then `a` is a divisor of `b`. This theorem is a fundamental property of integral division.
More concisely: For integers `a` and `b`, `a` divides `b` if and only if `b` mod `a` = 0.
|
Int.mul_ediv_cancel'
theorem Int.mul_ediv_cancel' : ∀ {a b : ℤ}, a ∣ b → a * (b / a) = b
This theorem states that for any two integers 'a' and 'b', if 'a' divides 'b' then 'a' times the integer division of 'b' by 'a' equals 'b'. In other words, if you perform integer division of 'b' by 'a' and then multiply the result by 'a', you'll get 'b' back, assuming 'a' is a divisor of 'b'. This is a fundamental property of integer division.
More concisely: If an integer a divides another integer b, then a * (b / a) = b.
|
Int.emod_emod_of_dvd
theorem Int.emod_emod_of_dvd : ∀ (n : ℤ) {m k : ℤ}, m ∣ k → n % k % m = n % m
This theorem, `Int.emod_emod_of_dvd`, states that for any integer `n` and any two integers `m` and `k`, if `m` divides `k`, then the remainder when `n` is divided by `k`, further divided by `m`, is equal to the remainder when `n` is divided by `m`. In mathematical notation, if `m|k`, then `(n mod k) mod m = n mod m`.
More concisely: If `m` divides `k`, then `(n mod k) mod m = n mod m` for any integer `n`.
|
Int.ediv_eq_of_eq_mul_right
theorem Int.ediv_eq_of_eq_mul_right : ∀ {a b c : ℤ}, b ≠ 0 → a = b * c → a / b = c
This theorem states that for any three integers 'a', 'b', and 'c', if 'b' is not zero and 'a' is equal to the product of 'b' and 'c', then the integer division of 'a' by 'b' is equal to 'c'. Essentially, it formalizes the intuitive property of division being the reverse operation of multiplication in the context of integers.
More concisely: If integers $a$, $b$ have $b \neq 0$ and $a = b \cdot c$, then $\frac{a}{b} = c$.
|
Int.emod_add_ediv
theorem Int.emod_add_ediv : ∀ (a b : ℤ), a % b + b * (a / b) = a
This theorem states that for all integer numbers `a` and `b`, the remainder of `a` divided by `b` added to `b` times the integer division of `a` by `b` equals `a`. In terms of mathematical notation, this would be: for all integers a and b, a % b + b * ⌊a / b⌋ = a. This is a key property of the integer division operation and its corresponding remainder operation.
More concisely: For all integers `a` and `b`, the remainder of `a` divided by `b` is equal to `a` modulo `b` plus `b` times the quotient of `a` by `b`. (Or, more succinctly: `a % b = a // b * b + a % b`)
|
Int.dvd_refl
theorem Int.dvd_refl : ∀ (n : ℤ), n ∣ n
The theorem `Int.dvd_refl` states that for every integer `n`, `n` divides `n`. In other words, any integer is a divisor of itself. This result is a fundamental property of integers in the realm of number theory.
More concisely: For every integer `n`, `n` divides `n`. In other words, `n` | `n` for all integers `n`.
|