Int.negOnePow_neg
theorem Int.negOnePow_neg : ∀ (n : ℤ), (-n).negOnePow = n.negOnePow
This theorem states that for all integers `n`, the negation of `n` raised to the power of negative one is equal to `n` raised to the power of negative one. In other words, negating the base does not affect the result when the base is raised to the power of negative one. This is expressed in mathematical notation as $(-n)^{-1} = n^{-1}$ for all integers `n`.
More concisely: For all integers `n`, the negative of the base raises to the power of negative one is equal to the base raised to the power of negative one, i.e., $(-n)^{-1} = n^{-1}$.
|
Int.negOnePow_even
theorem Int.negOnePow_even : ∀ (n : ℤ), Even n → n.negOnePow = 1
The theorem `Int.negOnePow_even` states that for any integer `n`, if `n` is even (i.e., there exists another integer `r` such that `n = r + r`), then raising `-1` to the power of `n` yields `1`. In other words, the negative one raised to any even integer power is equal to one.
More concisely: For any even integer `n`, $-1$ raised to the power of `n` equals 1.
|
Int.negOnePow_add
theorem Int.negOnePow_add : ∀ (n₁ n₂ : ℤ), (n₁ + n₂).negOnePow = n₁.negOnePow * n₂.negOnePow
This theorem states that for any two given integers `n₁` and `n₂`, the power of negative one to the sum of these integers is equal to the product of the power of negative one to `n₁` and the power of negative one to `n₂`. In mathematical terms, this theorem establishes that $(-1)^{n₁ + n₂} = (-1)^{n₁} * (-1)^{n₂}$.
More concisely: The theorem asserts that for any integers `n₁` and `n₂`, $(-1)^{n₁ + n₂} = (-1)^{n₁} \times (-1)^{n₂}$.
|
Int.negOnePow_odd
theorem Int.negOnePow_odd : ∀ (n : ℤ), Odd n → n.negOnePow = -1
This theorem states that for any integer `n`, if `n` is odd (meaning there exists an integer `k` such that `n = 2 * k + 1`), then the result of raising `-1` to the power of `n` (denoted by `n.negOnePow`) is equal to `-1`. Essentially, it's capturing the mathematical fact that -1 raised to any odd integer power is always -1.
More concisely: For any integer `n`, if `n` is odd then `(-1 : ℕ) ^ n = -1`.
|