Documentation

Mathlib.NumberTheory.Multiplicity

Multiplicity in Number Theory #

This file contains results in number theory relating to multiplicity.

Main statements #

References #

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 iFinset.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 iFinset.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 iFinset.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 iFinset.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 iFinset.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) (iFinset.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 : 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) + multiplicity p n

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) + multiplicity p n
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) + multiplicity p n
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) + 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 = (iFinset.range n, (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) + 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 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) + padicValNat p n
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) + padicValNat p n