# 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 #

theorem dvd_geom_sum₂_iff_of_dvd_sub {R : Type u_1} {n : } [] {x : R} {y : R} {p : R} (h : p x - y) :
p i, x ^ i * y ^ (n - 1 - i) p n * y ^ (n - 1)
theorem dvd_geom_sum₂_iff_of_dvd_sub' {R : Type u_1} {n : } [] {x : R} {y : R} {p : R} (h : p x - y) :
p i, x ^ i * y ^ (n - 1 - i) p n * x ^ (n - 1)
theorem dvd_geom_sum₂_self {R : Type u_1} {n : } [] {x : R} {y : R} (h : n x - y) :
n i, x ^ i * y ^ (n - 1 - i)
theorem sq_dvd_add_pow_sub_sub {R : Type u_1} [] (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 : } [] {x : R} {y : R} {p : R} (hp : ) (hxy : p x - y) (hx : ¬p x) (hn : ¬p n) :
¬p i, x ^ i * y ^ (n - 1 - i)
theorem odd_sq_dvd_geom_sum₂_sub {R : Type u_1} [] (a : R) (b : R) {p : } (hp : Odd p) :
p ^ 2 i, (a + p * b) ^ i * a ^ (p - 1 - i) - p * a ^ (p - 1)
theorem multiplicity.pow_sub_pow_of_prime {R : Type u_1} [] [] [DecidableRel fun (x x_1 : R) => x x_1] {p : R} (hp : ) {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} [] {x : R} {y : R} {p : } [] [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, x ^ i * y ^ (p - 1 - i)) = 1
theorem multiplicity.pow_prime_sub_pow_prime {R : Type u_1} [] {x : R} {y : R} {p : } [] [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} [] {x : R} {y : R} {p : } [] [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 : p.Prime) (hp1 : Odd p) {x : } {y : } (hxy : p x - y) (hx : ¬p x) (n : ) :
multiplicity (p) (x ^ n - y ^ n) = multiplicity (p) (x - y) +

Lifting the exponent lemma for odd primes.

theorem multiplicity.Int.pow_add_pow {p : } (hp : p.Prime) (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) +
theorem multiplicity.Nat.pow_sub_pow {p : } (hp : p.Prime) (hp1 : Odd p) {x : } {y : } (hxy : p x - y) (hx : ¬p x) (n : ) :
multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y) +
theorem multiplicity.Nat.pow_add_pow {p : } (hp : p.Prime) (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) +
theorem pow_two_pow_sub_pow_two_pow {R : Type u_1} [] {x : R} {y : R} (n : ) :
x ^ 2 ^ n - y ^ 2 ^ n = (i, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
theorem Int.sq_mod_four_eq_one_of_odd {x : } :
Odd xx ^ 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) +
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) +
theorem padicValNat.pow_sub_pow {x : } {y : } {p : } [hp : Fact p.Prime] (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) +
theorem padicValNat.pow_add_pow {x : } {y : } {p : } [hp : Fact p.Prime] (hp1 : Odd p) (hxy : p x + y) (hx : ¬p x) {n : } (hn : Odd n) :
padicValNat p (x ^ n + y ^ n) = padicValNat p (x + y) +