Int.natAbs_pow_two
theorem Int.natAbs_pow_two : ∀ (x : ℤ), ↑x.natAbs ^ 2 = x ^ 2
This theorem, referred to as `Int.natAbs_pow_two`, states that for all integers `x`, the square of the absolute value of `x` (expressed as a non-negative integer) is equal to the square of `x` itself. In mathematical terms, for any integer \(x\), \(|x|^2 = x^2\).
More concisely: For all integers x, |x|^2 = x^2.
|
Int.natAbs_sq
theorem Int.natAbs_sq : ∀ (x : ℤ), ↑x.natAbs ^ 2 = x ^ 2
The theorem `Int.natAbs_sq` states that for every integer `x`, the square of the absolute value of `x` (expressed as a natural number) is equal to the square of `x` itself. In other words, squaring the absolute value of an integer gives the same result as squaring the integer itself. This is a formalization of the mathematical fact that squaring a negative number yields the same result as squaring its positive counterpart, as squaring involves multiplication of the number by itself, rendering the sign irrelevant.
More concisely: For every integer x, |x|^2 = x^2.
|
Int.neg_succ
theorem Int.neg_succ : ∀ (a : ℤ), -a.succ = (-a).pred
The theorem `Int.neg_succ` states that for any integer `a`, the negation of the immediate successor of `a` is equal to the immediate predecessor of the negation of `a`. In mathematical terms, it says that for all integers $a$, $- (a + 1) = (-a) - 1$.
More concisely: The theorem `Int.neg_succ` asserts that for all integers $a$, $-(a + 1) = (-a) - 1$.
|
Int.coe_nat_nonneg
theorem Int.coe_nat_nonneg : ∀ (n : ℕ), 0 ≤ ↑n
This theorem, "Int.coe_nat_nonneg", is an alias of "Int.natCast_nonneg". The theorem states that for any natural number 'n', the integer representation of 'n' is always nonnegative, i.e., greater than or equal to zero. In other words, when you cast a natural number to an integer in Lean, the resulting integer is always nonnegative.
More concisely: For any natural number n, the integer representation of n is nonnegative. In Lean, this is expressed as the theorem Int.coe_nat_nonneg (or Int.natCast_nonneg) stating that the coercion from nat to int is non-negative.
|
Int.toNat_coe_nat
theorem Int.toNat_coe_nat : ∀ (n : ℕ), (↑n).toNat = n
This theorem, known as `Int.toNat_coe_nat`, states that for any natural number `n`, when `n` is cast to an integer and then converted to a natural number using the `Int.toNat` function, the resulting value is `n` itself. In other words, the process of casting a natural number to an integer and then converting it back to a natural number via `Int.toNat` is a no-op for all natural numbers.
More concisely: For all natural numbers `n`, `Int.toNat (Int.of Nat n) = n`.
|
Int.induction_on
theorem Int.induction_on :
∀ {p : ℤ → Prop} (i : ℤ), p 0 → (∀ (i : ℕ), p ↑i → p (↑i + 1)) → (∀ (i : ℕ), p (-↑i) → p (-↑i - 1)) → p i := by
sorry
This theorem, `Int.induction_on`, states that for any predicate `p` that applies to integers, if `p` holds for the integer `0`, and if for any natural number `i`, `p` holding for `i` implies that `p` holds for `i+1`, and also if `p` holding for `-i` implies that `p` holds for `-i-1`, then `p` holds for every integer `i`. In other words, it's an induction principle for integers, including both non-negative and negative numbers.
More concisely: The theorem `Int.induction_on` asserts that a predicate on integers holds for all integers if it holds for zero and is closed under successor and predecessor.
|