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 : R} {y : R} {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 : R} {y : R} {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 : R} {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 : R) (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 : R} {y : R} {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 : R) (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 multiplicity.pow_sub_pow_of_prime {R : Type u_1} [CommRing R] [IsDomain R] [DecidableRel fun (x x_1 : R) => x ∣ x_1] {p : R} (hp : Prime p) {x : R} {y : R} (hxy : p ∣ x - y) (hx : ¬p ∣ x) {n : ℕ} (hn : ¬p ∣ ↑n) : multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y)

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

theorem multiplicity.pow_prime_sub_pow_prime {R : Type u_1} [CommRing R] {x : R} {y : R} {p : ℕ} [IsDomain R] [DecidableRel fun (x x_1 : R) => x ∣ x_1] (hp : Prime ↑p) (hp1 : Odd p) (hxy : ↑p ∣ x - y) (hx : ¬↑p ∣ x) : multiplicity (↑p) (x ^ p - y ^ p) = multiplicity (↑p) (x - y) + 1

theorem multiplicity.pow_prime_pow_sub_pow_prime_pow {R : Type u_1} [CommRing R] {x : R} {y : R} {p : ℕ} [IsDomain R] [DecidableRel fun (x x_1 : R) => x ∣ x_1] (hp : Prime ↑p) (hp1 : Odd p) (hxy : ↑p ∣ x - y) (hx : ¬↑p ∣ x) (a : ℕ) : multiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = multiplicity (↑p) (x - y) + ↑a

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

Lifting the exponent lemma for odd primes.

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

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

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

theorem pow_two_pow_sub_pow_two_pow {R : Type u_1} [CommRing R] {x : R} {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.two_pow_two_pow_add_two_pow_two_pow {x : ℤ} {y : ℤ} (hx : ¬2 ∣ x) (hxy : 4 ∣ x - y) (i : ℕ) : multiplicity 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) : multiplicity 2 (x ^ 2 ^ n - y ^ 2 ^ n) = multiplicity 2 (x - y) + ↑n

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

theorem Int.two_pow_sub_pow {x : ℤ} {y : ℤ} {n : ℕ} (hxy : 2 ∣ x - y) (hx : ¬2 ∣ x) (hn : Even n) : multiplicity 2 (x ^ n - y ^ n) + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 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) : multiplicity 2 (x ^ n - y ^ n) + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 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_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