# mathlib3documentation

number_theory.multiplicity

# Multiplicity in Number Theory #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : } [comm_ring R] {x y p : R} (h : p x - y) :
p (finset.range n).sum (λ (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 : } [comm_ring R] {x y p : R} (h : p x - y) :
p (finset.range n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i)) p n * x ^ (n - 1)
theorem dvd_geom_sum₂_self {R : Type u_1} {n : } [comm_ring R] {x y : R} (h : n x - y) :
n (finset.range n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i))
theorem sq_dvd_add_pow_sub_sub {R : Type u_1} [comm_ring 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 : } [comm_ring R] {x y p : R} (hp : prime p) (hxy : p x - y) (hx : ¬p x) (hn : ¬p n) :
¬p (finset.range n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i))
theorem odd_sq_dvd_geom_sum₂_sub {R : Type u_1} [comm_ring R] (a b : R) {p : } (hp : odd p) :
p ^ 2 (finset.range p).sum (λ (i : ), (a + p * b) ^ i * a ^ (p - 1 - i)) - p * a ^ (p - 1)
theorem multiplicity.pow_sub_pow_of_prime {R : Type u_1} [comm_ring R] [is_domain R] {p : R} (hp : prime p) {x y : R} (hxy : p x - y) (hx : ¬p x) {n : } (hn : ¬p n) :
(x ^ n - y ^ n) = (x - y)
theorem multiplicity.geom_sum₂_eq_one {R : Type u_1} [comm_ring R] {x y : R} {p : } [is_domain R] (hp : prime p) (hp1 : odd p) (hxy : p x - y) (hx : ¬p x) :
((finset.range p).sum (λ (i : ), x ^ i * y ^ (p - 1 - i))) = 1
theorem multiplicity.pow_prime_sub_pow_prime {R : Type u_1} [comm_ring R] {x y : R} {p : } [is_domain R] (hp : prime p) (hp1 : odd p) (hxy : p x - y) (hx : ¬p x) :
(x ^ p - y ^ p) = (x - y) + 1
theorem multiplicity.pow_prime_pow_sub_pow_prime_pow {R : Type u_1} [comm_ring R] {x y : R} {p : } [is_domain R] (hp : prime p) (hp1 : odd p) (hxy : p x - y) (hx : ¬p x) (a : ) :
(x ^ p ^ a - y ^ p ^ a) = (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 : ) :
(x ^ n - y ^ n) = (x - y) + 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) :
(x ^ n + y ^ n) = (x + y) + 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 : ) :
(x ^ n - y ^ n) = (x - y) + 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) :
(x ^ n + y ^ n) = (x + y) + n
theorem pow_two_pow_sub_pow_two_pow {R : Type u_1} [comm_ring R] {x y : R} (n : ) :
x ^ 2 ^ n - y ^ 2 ^ n = (finset.range n).prod (λ (i : ), 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 : ) :
(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) :
(x ^ 2 ^ n - y ^ 2 ^ n) = (x - y) + n
theorem int.two_pow_sub_pow' {x y : } (n : ) (hxy : 4 x - y) (hx : ¬2 x) :
(x ^ n - y ^ n) = (x - y) +
theorem int.two_pow_sub_pow {x y : } {n : } (hxy : 2 x - y) (hx : ¬2 x) (hn : even n) :
(x ^ n - y ^ n) + 1 = (x + y) + (x - y) +

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) :
(x ^ n - y ^ n) + 1 = (x + y) + (x - y) + n
theorem padic_val_nat.pow_two_sub_pow {x y : } (hyx : y < x) (hxy : 2 x - y) (hx : ¬2 x) {n : } (hn : 0 < n) (hneven : even n) :
(x ^ n - y ^ n) + 1 = (x + y) + (x - y) +
theorem padic_val_nat.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 : 0 < n) :
(x ^ n - y ^ n) = (x - y) +
theorem padic_val_nat.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) :
(x ^ n + y ^ n) = (x + y) +