Int.cast_id
theorem Int.cast_id : ∀ {n : ℤ}, ↑n = n
This theorem, `Int.cast_id`, states that for every integer `n`, the cast of `n` to an integer is equal to `n` itself. In other words, performing an integer-to-integer cast doesn't change the value, for all integers. This is expressed in Lean 4 using the universal quantifier `∀` and the equality operator `=`.
More concisely: For all integers n, the cast of n to an integer is equal to n itself. (Or equivalently, the integer conversion operation is the identity function on integers.)
|
Int.natAbs_pow
theorem Int.natAbs_pow : ∀ (n : ℤ) (k : ℕ), (n ^ k).natAbs = n.natAbs ^ k
This theorem, `Int.natAbs_pow`, states that for any integer `n` and any natural number `k`, the absolute value of `n` raised to the power of `k` is equal to the absolute value of `n` itself raised to the power of `k`. In other words, if you first apply the power operation to an integer and then take the absolute value, you get the same result as if you first took the absolute value and then applied the power operation. We can write this mathematically as: $\left| n^k \right| = \left| n \right|^k$ for all integer `n` and natural number `k`.
More concisely: For all integers `n` and natural numbers `k`, the absolute value of `n` raised to the power of `k` equals the absolute value of `n` raised to the power of `k`. In mathematical notation: $|n^k| = |n|^k$.
|