Int.emod_lt
theorem Int.emod_lt : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → a % b < |b|
This theorem states that for any integer `a` and any non-zero integer `b`, the remainder of `a` divided by `b` (denoted as `a % b`) is less than the absolute value of `b` (denoted as `|b|`). This is a formalization of the standard property of modulus in arithmetic, asserting that the remainder when a number is divided by another is always less than the divisor, in absolute value.
More concisely: For any integers `a` and `b` with `b` non-zero, `|a % b| < |b|`.
|
Int.le_induction_down
theorem Int.le_induction_down : ∀ {P : ℤ → Prop} {m : ℤ}, P m → (∀ n ≤ m, P n → P (n - 1)) → ∀ n ≤ m, P n
This theorem states that for any integer-valued property `P` and any integer `m`, if `P m` is true and for all `n` less than or equal to `m`, `P n` implies `P (n - 1)`, then `P n` is true for all `n` less than or equal to `m`. This is essentially a form of mathematical induction that works downwards from `m`.
More concisely: If an integer-valued property `P` holds for `m` and `P n` implies `P (n - 1)` for all `n` from `m` down to `1`, then `P` holds for all integers `n` from `m` down to `1`.
|
Int.natAbs_le_self_pow_two
theorem Int.natAbs_le_self_pow_two : ∀ (a : ℤ), ↑a.natAbs ≤ a ^ 2
This theorem, named `Int.natAbs_le_self_pow_two`, states that for any integer `a`, the absolute value of `a` when converted to a natural number (expressed as `a.natAbs`) is always less than or equal to the square of `a` (expressed as `a ^ 2`).
More concisely: For all integers a, |a| ≤ a ^ 2, where |a| denotes the absolute value of a.
|
Int.toNat_le
theorem Int.toNat_le : ∀ {a : ℤ} {n : ℕ}, a.toNat ≤ n ↔ a ≤ ↑n
The theorem `Int.toNat_le` states that for any integer `a` and natural number `n`, the function `Int.toNat` applied to `a` is less than or equal to `n` if and only if `a` is less than or equal to `n` when `n` is considered as an integer. In other words, turning `a` into a natural number via `Int.toNat` and comparing it to `n` is equivalent to directly comparing `a` and `n` in the integer domain. This establishes a relationship between integer-to-natural number conversion and inequality comparison in Lean 4.
More concisely: For any integer `a` and natural number `n`, `Int.toNat a <= n` if and only if `a <= n` in the integer domain.
|
Int.toNat_sub_of_le
theorem Int.toNat_sub_of_le : ∀ {a b : ℤ}, b ≤ a → ↑(a - b).toNat = a - b
The theorem `Int.toNat_sub_of_le` states that for any two integers `a` and `b`, if `b` is less than or equal to `a`, then converting the difference `a - b` to a natural number and then back to an integer gives back `a - b`. In other words, if `b` is less than or equal to `a`, the subtraction operation `a - b` is preserved through the process of conversion to a natural number and back.
More concisely: If `a` is an integer and `b` is a natural number less than or equal to `a`, then `Int.toNat a.toNat >> Nat.sub << Nat.toInt b = a - b`.
|
Int.le_induction
theorem Int.le_induction :
∀ {P : ℤ → Prop} {m : ℤ}, P m → (∀ (n : ℤ), m ≤ n → P n → P (n + 1)) → ∀ (n : ℤ), m ≤ n → P n
This theorem, 'Int.le_induction', is a principle of mathematical induction for integers. It states that for any property 'P' defined on integers, if 'P' holds for an integer 'm', and if 'P' also holds for any integer 'n' greater than or equal to 'm' implies that 'P' holds for 'n+1', then 'P' holds for all integers 'n' that are greater than or equal to 'm'. This theorem is an important tool in proofs involving properties of integers.
More concisely: The theorem 'Int.le_induction' asserts that if a property 'P' holds for an integer 'm' and is closed under the successor function, then 'P' holds for all integers greater than or equal to 'm'.
|
Int.abs_eq_natAbs
theorem Int.abs_eq_natAbs : ∀ (a : ℤ), |a| = ↑a.natAbs
The theorem `Int.abs_eq_natAbs` states that for every integer `a`, the absolute value of `a`, denoted as `|a|`, is equal to the natural number corresponding to the absolute value of `a` computed using the `Int.natAbs` function. The `Int.natAbs` function takes an integer input and returns its absolute value as a natural number. For positive integers and zero, it returns the integer itself, and for negative integers, it returns the positive counterpart.
More concisely: For every integer `a`, the absolute value `|a|` is equal to the natural number `Int.natAbs a`.
|
Int.abs_lt_one_iff
theorem Int.abs_lt_one_iff : ∀ {a : ℤ}, |a| < 1 ↔ a = 0
This theorem states that for any integer `a`, the absolute value of `a` is less than 1 if and only if `a` equals 0. In other words, the only integer that has an absolute value strictly less than 1 is 0, and conversely, if an integer has an absolute value strictly less than 1, it must be 0.
More concisely: For any integer `a`, |a| < 1 if and only if a = 0.
|
Int.le_self_pow_two
theorem Int.le_self_pow_two : ∀ (b : ℤ), b ≤ b ^ 2
This theorem, `Int.le_self_pow_two`, states that for all integers `b`, `b` is less than or equal to its square (i.e., `b ^ 2`). In other words, the square of any integer is always greater than or equal to the integer itself.
More concisely: For all integers `b`, `b` is less than or equal to `b`^2`.
|
Int.le_sub_one_iff
theorem Int.le_sub_one_iff : ∀ {a b : ℤ}, a ≤ b - 1 ↔ a < b
This theorem states that for any two integers `a` and `b`, the condition `a` being less than or equal to `b - 1` is equivalent to `a` being strictly less than `b`. This can be seen as a way of expressing strict inequality (`<`) in terms of a non-strict inequality (`≤`) with an offset of `-1` on one side.
More concisely: For any integers `a` and `b`, `a ≤ b - 1` if and only if `a < b`.
|
Int.toNat_lt_toNat
theorem Int.toNat_lt_toNat : ∀ {a b : ℤ}, 0 < b → (a.toNat < b.toNat ↔ a < b)
This theorem, `Int.toNat_lt_toNat`, states that for all integers `a` and `b`, if `b` is greater than 0, then the equivalent natural number of `a` is less than the equivalent natural number of `b` if and only if `a` is less than `b`. In other words, the relationship of "less than" between `a` and `b` is preserved when both integers are converted to their natural number counterparts using the `Int.toNat` function, but this is only guaranteed when `b` is positive.
More concisely: For all integers `a` and `b` with `b` positive, `Int.toNat a < Int.toNat b` if and only if `a < b`.
|