mathlib3 documentation

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 #

References #

source
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)
source
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)
source
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))
source
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
source
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))
source
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)
source
theorem multiplicity.pow_sub_pow_of_prime {R : Type u_1} [comm_ring R] [is_domain R] [decidable_rel has_dvd.dvd] {p : R} (hp : prime p) {x y : R} (hxy : p ∣ x - y) (hx : ¬p ∣ x) {n : ℕ} (hn : ¬p ∣ ↑n) :
multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y)
source
theorem multiplicity.geom_sum₂_eq_one {R : Type u_1} [comm_ring R] {x y : R} {p : ℕ} [is_domain R] [decidable_rel has_dvd.dvd] (hp : prime ↑p) (hp1 : odd p) (hxy : ↑p ∣ x - y) (hx : ¬↑p ∣ x) :
multiplicity ↑p ((finset.range p).sum (λ (i : ℕ), x ^ i * y ^ (p - 1 - i))) = 1
source
theorem multiplicity.pow_prime_sub_pow_prime {R : Type u_1} [comm_ring R] {x y : R} {p : ℕ} [is_domain R] [decidable_rel has_dvd.dvd] (hp : prime ↑p) (hp1 : odd p) (hxy : ↑p ∣ x - y) (hx : ¬↑p ∣ x) :
multiplicity ↑p (x ^ p - y ^ p) = multiplicity ↑p (x - y) + 1
source
theorem multiplicity.pow_prime_pow_sub_pow_prime_pow {R : Type u_1} [comm_ring R] {x y : R} {p : ℕ} [is_domain R] [decidable_rel has_dvd.dvd] (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
source
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.

source
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
source
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
source
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
source
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)
source
theorem int.sq_mod_four_eq_one_of_odd {x : ℤ} :
odd x → x ^ 2 % 4 = 1
source
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
source
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
source
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
source
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

source
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
source
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) :
padic_val_nat 2 (x ^ n - y ^ n) + 1 = padic_val_nat 2 (x + y) + padic_val_nat 2 (x - y) + padic_val_nat 2 n
source
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) :
padic_val_nat p (x ^ n - y ^ n) = padic_val_nat p (x - y) + padic_val_nat p n
source
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) :
padic_val_nat p (x ^ n + y ^ n) = padic_val_nat p (x + y) + padic_val_nat p n