Multiplicity in Number Theory

This file contains results in number theory relating to multiplicity.

Main statements

• multiplicity.Int.pow_sub_pow is the lifting the exponent lemma for odd primes. We also prove several variations of the lemma.

References

• [Wikipedia, Lifting-the-exponent lemma] (https://en.wikipedia.org/wiki/Lifting-the-exponent_lemma)

theorem dvd_geom_sum₂_iff_of_dvd_sub {R : Type u_1} {n : ℕ} [CommRing R] {x y p : R} (h : p ∣ x - y) : p ∣ ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * y ^ (n - 1)

theorem dvd_geom_sum₂_iff_of_dvd_sub' {R : Type u_1} {n : ℕ} [CommRing R] {x y p : R} (h : p ∣ x - y) : p ∣ ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * x ^ (n - 1)

theorem dvd_geom_sum₂_self {R : Type u_1} {n : ℕ} [CommRing R] {x y : R} (h : ↑n ∣ x - y) : ↑n ∣ ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)

theorem sq_dvd_add_pow_sub_sub {R : Type u_1} [CommRing R] (p x : R) (n : ℕ) : p ^ 2 ∣ (x + p) ^ n - x ^ (n - 1) * p * ↑n - x ^ n

theorem not_dvd_geom_sum₂ {R : Type u_1} {n : ℕ} [CommRing R] {x y p : R} (hp : Prime p) (hxy : p ∣ x - y) (hx : ¬p ∣ x) (hn : ¬p ∣ ↑n) : ¬p ∣ ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)

theorem odd_sq_dvd_geom_sum₂_sub {R : Type u_1} [CommRing R] (a b : R) {p : ℕ} (hp : Odd p) : ↑p ^ 2 ∣ ∑ i ∈ Finset.range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i) - ↑p * a ^ (p - 1)

theorem emultiplicity_pow_sub_pow_of_prime {R : Type u_1} [CommRing R] [IsDomain R] {p : R} (hp : Prime p) {x y : R} (hxy : p ∣ x - y) (hx : ¬p ∣ x) {n : ℕ} (hn : ¬p ∣ ↑n) : emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y)

theorem emultiplicity_geom_sum₂_eq_one {R : Type u_1} [CommRing R] {x y : R} {p : ℕ} [IsDomain R] (hp : Prime ↑p) (hp1 : Odd p) (hxy : ↑p ∣ x - y) (hx : ¬↑p ∣ x) : emultiplicity (↑p) (∑ i ∈ Finset.range p, x ^ i * y ^ (p - 1 - i)) = 1

theorem emultiplicity_pow_prime_sub_pow_prime {R : Type u_1} [CommRing R] {x y : R} {p : ℕ} [IsDomain R] (hp : Prime ↑p) (hp1 : Odd p) (hxy : ↑p ∣ x - y) (hx : ¬↑p ∣ x) : emultiplicity (↑p) (x ^ p - y ^ p) = emultiplicity (↑p) (x - y) + 1

theorem emultiplicity_pow_prime_pow_sub_pow_prime_pow {R : Type u_1} [CommRing R] {x y : R} {p : ℕ} [IsDomain R] (hp : Prime ↑p) (hp1 : Odd p) (hxy : ↑p ∣ x - y) (hx : ¬↑p ∣ x) (a : ℕ) : emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p) (x - y) + ↑a

theorem Int.emultiplicity_pow_sub_pow {p : ℕ} (hp : Nat.Prime p) (hp1 : Odd p) {x y : ℤ} (hxy : ↑p ∣ x - y) (hx : ¬↑p ∣ x) (n : ℕ) : emultiplicity (↑p) (x ^ n - y ^ n) = emultiplicity (↑p) (x - y) + emultiplicity p n

Lifting the exponent lemma for odd primes.

theorem Int.emultiplicity_pow_add_pow {p : ℕ} (hp : Nat.Prime p) (hp1 : Odd p) {x y : ℤ} (hxy : ↑p ∣ x + y) (hx : ¬↑p ∣ x) {n : ℕ} (hn : Odd n) : emultiplicity (↑p) (x ^ n + y ^ n) = emultiplicity (↑p) (x + y) + emultiplicity p n

theorem Nat.emultiplicity_pow_sub_pow {p : ℕ} (hp : Prime p) (hp1 : Odd p) {x y : ℕ} (hxy : p ∣ x - y) (hx : ¬p ∣ x) (n : ℕ) : emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n

theorem Nat.emultiplicity_pow_add_pow {p : ℕ} (hp : Prime p) (hp1 : Odd p) {x y : ℕ} (hxy : p ∣ x + y) (hx : ¬p ∣ x) {n : ℕ} (hn : Odd n) : emultiplicity p (x ^ n + y ^ n) = emultiplicity p (x + y) + emultiplicity p n

theorem pow_two_pow_sub_pow_two_pow {R : Type u_1} [CommRing R] {x y : R} (n : ℕ) : x ^ 2 ^ n - y ^ 2 ^ n = (∏ i ∈ Finset.range n, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)

theorem Int.sq_mod_four_eq_one_of_odd {x : ℤ} : Odd x → x ^ 2 % 4 = 1

theorem Int.eight_dvd_sq_sub_one_of_odd {k : ℤ} (hk : Odd k) : 8 ∣ k ^ 2 - 1

theorem Nat.eight_dvd_sq_sub_one_of_odd {k : ℕ} (hk : Odd k) : 8 ∣ k ^ 2 - 1

theorem Int.two_pow_two_pow_add_two_pow_two_pow {x y : ℤ} (hx : ¬2 ∣ x) (hxy : 4 ∣ x - y) (i : ℕ) : emultiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1

theorem Int.two_pow_two_pow_sub_pow_two_pow {x y : ℤ} (n : ℕ) (hxy : 4 ∣ x - y) (hx : ¬2 ∣ x) : emultiplicity 2 (x ^ 2 ^ n - y ^ 2 ^ n) = emultiplicity 2 (x - y) + ↑n

theorem Int.two_pow_sub_pow' {x y : ℤ} (n : ℕ) (hxy : 4 ∣ x - y) (hx : ¬2 ∣ x) : emultiplicity 2 (x ^ n - y ^ n) = emultiplicity 2 (x - y) + emultiplicity 2 ↑n

theorem Int.two_pow_sub_pow {x y : ℤ} {n : ℕ} (hxy : 2 ∣ x - y) (hx : ¬2 ∣ x) (hn : Even n) : emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 ↑n

Lifting the exponent lemma for p = 2

theorem Nat.two_pow_sub_pow {x y : ℕ} (hxy : 2 ∣ x - y) (hx : ¬2 ∣ x) {n : ℕ} (hn : Even n) : emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

theorem padicValNat.pow_two_sub_pow {x y : ℕ} (hyx : y < x) (hxy : 2 ∣ x - y) (hx : ¬2 ∣ x) {n : ℕ} (hn : n ≠ 0) (hneven : Even n) : padicValNat 2 (x ^ n - y ^ n) + 1 = padicValNat 2 (x + y) + padicValNat 2 (x - y) + padicValNat 2 n

theorem padicValNat.pow_two_sub_one {x n : ℕ} (h1x : 1 < x) (hx : ¬2 ∣ x) (hn : n ≠ 0) (hneven : Even n) : padicValNat 2 (x ^ n - 1) + 1 = padicValNat 2 (x + 1) + padicValNat 2 (x - 1) + padicValNat 2 n

theorem padicValNat.pow_two_sub_one_ge {n x : ℕ} (h1x : 1 < x) (hx : ¬2 ∣ x) (hn : n ≠ 0) (hneven : Even n) : padicValNat 2 n + 2 ≤ padicValNat 2 (x ^ n - 1)

theorem padicValNat.pow_sub_pow {x y p : ℕ} [hp : Fact (Nat.Prime p)] (hp1 : Odd p) (hyx : y < x) (hxy : p ∣ x - y) (hx : ¬p ∣ x) {n : ℕ} (hn : n ≠ 0) : padicValNat p (x ^ n - y ^ n) = padicValNat p (x - y) + padicValNat p n

theorem padicValNat.pow_add_pow {x y p : ℕ} [hp : Fact (Nat.Prime p)] (hp1 : Odd p) (hxy : p ∣ x + y) (hx : ¬p ∣ x) {n : ℕ} (hn : Odd n) : padicValNat p (x ^ n + y ^ n) = padicValNat p (x + y) + padicValNat p n