Int.two_pow_sub_pow
theorem Int.two_pow_sub_pow :
∀ {x y : ℤ} {n : ℕ},
2 ∣ x - y →
¬2 ∣ x →
Even n →
multiplicity 2 (x ^ n - y ^ n) + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 2 ↑n
The "Lifting the exponent lemma" for `p = 2` states that for any integers `x` and `y`, and a natural number `n` that is even, if `2` divides `(x - y)` but does not divide `x`, then the multiplicity of `2` in `(x^n - y^n) + 1` equals the sum of the multiplicities of `2` in `(x + y)`, `(x - y)`, and `n`. In other words, this theorem describes a condition where the number of powers of `2` that exactly divide `(x^n - y^n) + 1` equals the sum of the numbers of powers of `2` that exactly divide each of `(x + y)`, `(x - y)`, and `n`.
More concisely: For even natural number `n`, if `2` divides `(x - y)` but not `x`, then the number of powers of `2` in `(x^n - y^n) + 1` equals the sum of the powers of `2` in `(x + y)`, `(x - y)`, and `n`.
|
multiplicity.Int.pow_sub_pow
theorem multiplicity.Int.pow_sub_pow :
∀ {p : ℕ},
p.Prime →
Odd p →
∀ {x y : ℤ},
↑p ∣ x - y →
¬↑p ∣ x → ∀ (n : ℕ), multiplicity (↑p) (x ^ n - y ^ n) = multiplicity (↑p) (x - y) + multiplicity p n
The **Lifting the Exponent lemma** for odd primes states that for any prime number `p` that is odd, and for any two integers `x` and `y` such that `p` divides their difference `x-y` but `p` does not divide `x`, the multiplicity of `p` in the difference of `x^n` and `y^n` is equal to the sum of the multiplicity of `p` in `x-y` and the multiplicity of `p` in `n`. Here, the multiplicity of `p` in a number `a` refers to the largest natural number `n` such that `p^n` divides `a`.
More concisely: For odd prime numbers `p` and integers `x` and `y` with `p` dividing `x-y` but not `x`, the multiplicity of `p` in `x^n - y^n` is `n` times the multiplicity of `p` in `x-y`.
|