mathlib documentation

number_theory.divisors

Divisor finsets #

This file defines sets of divisors of a natural number. This is particularly useful as background for defining Dirichlet convolution.

Main Definitions #

Let n : ℕ. All of the following definitions are in the nat namespace:

Implementation details #

Tags #

divisors, perfect numbers

source
def nat.divisors (n : ℕ) :
finset ℕ

divisors n is the finset of divisors of n. As a special case, divisors 0 = ∅.

Equations
source
def nat.proper_divisors (n : ℕ) :
finset ℕ

proper_divisors n is the finset of divisors of n, other than n. As a special case, proper_divisors 0 = ∅.

Equations
source
def nat.divisors_antidiagonal (n : ℕ) :
finset (ℕ × ℕ)

divisors_antidiagonal n is the finset of pairs (x,y) such that x * y = n. As a special case, divisors_antidiagonal 0 = ∅.

Equations
source
theorem nat.proper_divisors.not_self_mem {n : ℕ} :
n ∉ n.proper_divisors
source
@[simp]
theorem nat.mem_proper_divisors {n m : ℕ} :
n ∈ m.proper_divisors ↔ n ∣ m ∧ n < m
source
theorem nat.divisors_eq_proper_divisors_insert_self_of_pos {n : ℕ} (h : 0 < n) :
n.divisors = insert n n.proper_divisors
source
@[simp]
theorem nat.mem_divisors {n m : ℕ} :
n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0
source
theorem nat.mem_divisors_self (n : ℕ) (h : n ≠ 0) :
n ∈ n.divisors
source
theorem nat.dvd_of_mem_divisors {n m : ℕ} (h : n ∈ m.divisors) :
n ∣ m
source
@[simp]
theorem nat.mem_divisors_antidiagonal {n : ℕ} {x : ℕ × ℕ} :
x ∈ n.divisors_antidiagonal ↔ (x.fst) * x.snd = n ∧ n ≠ 0
source
theorem nat.divisor_le {n m : ℕ} :
n ∈ m.divisors → n ≤ m
source
theorem nat.divisors_subset_of_dvd {n m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) :
m.divisors ⊆ n.divisors
source
theorem nat.divisors_subset_proper_divisors {n m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) (hdiff : m ≠ n) :
m.divisors ⊆ n.proper_divisors
source
@[simp]
theorem nat.divisors_zero  :
0.divisors = ∅
source
@[simp]
theorem nat.proper_divisors_zero  :
0.proper_divisors = ∅
source
theorem nat.proper_divisors_subset_divisors {n : ℕ} :
n.proper_divisors ⊆ n.divisors
source
@[simp]
theorem nat.divisors_one  :
1.divisors = {1}
source
@[simp]
theorem nat.proper_divisors_one  :
1.proper_divisors = ∅
source
theorem nat.pos_of_mem_divisors {n m : ℕ} (h : m ∈ n.divisors) :
0 < m
source
theorem nat.pos_of_mem_proper_divisors {n m : ℕ} (h : m ∈ n.proper_divisors) :
0 < m
source
theorem nat.one_mem_proper_divisors_iff_one_lt {n : ℕ} :
1 ∈ n.proper_divisors ↔ 1 < n
source
@[simp]
theorem nat.divisors_antidiagonal_zero  :
0.divisors_antidiagonal = ∅
source
@[simp]
theorem nat.divisors_antidiagonal_one  :
1.divisors_antidiagonal = {(1, 1)}
source
theorem nat.swap_mem_divisors_antidiagonal {n : ℕ} {x : ℕ × ℕ} (h : x ∈ n.divisors_antidiagonal) :
x.swap ∈ n.divisors_antidiagonal
source
theorem nat.fst_mem_divisors_of_mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} (h : x ∈ n.divisors_antidiagonal) :
x.fst ∈ n.divisors
source
theorem nat.snd_mem_divisors_of_mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} (h : x ∈ n.divisors_antidiagonal) :
x.snd ∈ n.divisors
source
@[simp]
theorem nat.map_swap_divisors_antidiagonal {n : ℕ} :
finset.map {to_fun := prod.swap ℕ, inj' := _} n.divisors_antidiagonal = n.divisors_antidiagonal
source
theorem nat.sum_divisors_eq_sum_proper_divisors_add_self {n : ℕ} :
∑ (i : ℕ) in n.divisors, i = ∑ (i : ℕ) in n.proper_divisors, i + n
source
def nat.perfect (n : ℕ) :
Prop

n : ℕ is perfect if and only the sum of the proper divisors of n is n and n is positive.

Equations
source
theorem nat.perfect_iff_sum_proper_divisors {n : ℕ} (h : 0 < n) :
n.perfect ↔ ∑ (i : ℕ) in n.proper_divisors, i = n
source
theorem nat.perfect_iff_sum_divisors_eq_two_mul {n : ℕ} (h : 0 < n) :
n.perfect ↔ ∑ (i : ℕ) in n.divisors, i = 2 * n
source
theorem nat.mem_divisors_prime_pow {p : ℕ} (pp : nat.prime p) (k : ℕ) {x : ℕ} :
x ∈ (p ^ k).divisors ↔ ∃ (j : ℕ) (H : j ≤ k), x = p ^ j
source
theorem nat.prime.divisors {p : ℕ} (pp : nat.prime p) :
p.divisors = {1, p}
source
theorem nat.prime.proper_divisors {p : ℕ} (pp : nat.prime p) :
p.proper_divisors = {1}
source
theorem nat.divisors_prime_pow {p : ℕ} (pp : nat.prime p) (k : ℕ) :
(p ^ k).divisors = finset.map {to_fun := pow p, inj' := _} (finset.range (k + 1))
source
theorem nat.eq_proper_divisors_of_subset_of_sum_eq_sum {n : ℕ} {s : finset ℕ} (hsub : s ⊆ n.proper_divisors) :
∑ (x : ℕ) in s, x = ∑ (x : ℕ) in n.proper_divisors, x → s = n.proper_divisors
source
theorem nat.sum_proper_divisors_dvd {n : ℕ} (h : ∑ (x : ℕ) in n.proper_divisors, x ∣ n) :
∑ (x : ℕ) in n.proper_divisors, x = 1 ∨ ∑ (x : ℕ) in n.proper_divisors, x = n
source
@[simp]
theorem nat.prime.sum_proper_divisors {α : Type u_1} [add_comm_monoid α] {p : ℕ} {f : ℕ → α} (h : nat.prime p) :
∑ (x : ℕ) in p.proper_divisors, f x = f 1
source
@[simp]
theorem nat.prime.prod_proper_divisors {α : Type u_1} [comm_monoid α] {p : ℕ} {f : ℕ → α} (h : nat.prime p) :
∏ (x : ℕ) in p.proper_divisors, f x = f 1
source
@[simp]
theorem nat.prime.sum_divisors {α : Type u_1} [add_comm_monoid α] {p : ℕ} {f : ℕ → α} (h : nat.prime p) :
∑ (x : ℕ) in p.divisors, f x = f p + f 1
source
@[simp]
theorem nat.prime.prod_divisors {α : Type u_1} [comm_monoid α] {p : ℕ} {f : ℕ → α} (h : nat.prime p) :
∏ (x : ℕ) in p.divisors, f x = (f p) * f 1
source
theorem nat.proper_divisors_eq_singleton_one_iff_prime {n : ℕ} :
n.proper_divisors = {1} ↔ nat.prime n
source
theorem nat.sum_proper_divisors_eq_one_iff_prime {n : ℕ} :
∑ (x : ℕ) in n.proper_divisors, x = 1 ↔ nat.prime n
source
theorem nat.mem_proper_divisors_prime_pow {p : ℕ} (pp : nat.prime p) (k : ℕ) {x : ℕ} :
x ∈ (p ^ k).proper_divisors ↔ ∃ (j : ℕ) (H : j < k), x = p ^ j
source
theorem nat.proper_divisors_prime_pow {p : ℕ} (pp : nat.prime p) (k : ℕ) :
(p ^ k).proper_divisors = finset.map {to_fun := pow p, inj' := _} (finset.range k)
source
@[simp]
theorem nat.sum_proper_divisors_prime_nsmul {α : Type u_1} [add_comm_monoid α] {k p : ℕ} {f : ℕ → α} (h : nat.prime p) :
∑ (x : ℕ) in (p ^ k).proper_divisors, f x = ∑ (x : ℕ) in finset.range k, f (p ^ x)
source
@[simp]
theorem nat.prod_proper_divisors_prime_pow {α : Type u_1} [comm_monoid α] {k p : ℕ} {f : ℕ → α} (h : nat.prime p) :
∏ (x : ℕ) in (p ^ k).proper_divisors, f x = ∏ (x : ℕ) in finset.range k, f (p ^ x)
source
@[simp]
theorem nat.sum_divisors_prime_pow {α : Type u_1} [add_comm_monoid α] {k p : ℕ} {f : ℕ → α} (h : nat.prime p) :
∑ (x : ℕ) in (p ^ k).divisors, f x = ∑ (x : ℕ) in finset.range (k + 1), f (p ^ x)
source
@[simp]
theorem nat.prod_divisors_prime_pow {α : Type u_1} [comm_monoid α] {k p : ℕ} {f : ℕ → α} (h : nat.prime p) :
∏ (x : ℕ) in (p ^ k).divisors, f x = ∏ (x : ℕ) in finset.range (k + 1), f (p ^ x)
source
theorem nat.prod_divisors_antidiagonal {M : Type u_1} [comm_monoid M] (f : ℕ → ℕ → M) {n : ℕ} :
∏ (i : ℕ × ℕ) in n.divisors_antidiagonal, f i.fst i.snd = ∏ (i : ℕ) in n.divisors, f i (n / i)
source
theorem nat.sum_divisors_antidiagonal {M : Type u_1} [add_comm_monoid M] (f : ℕ → ℕ → M) {n : ℕ} :
∑ (i : ℕ × ℕ) in n.divisors_antidiagonal, f i.fst i.snd = ∑ (i : ℕ) in n.divisors, f i (n / i)
source
theorem nat.prod_divisors_antidiagonal' {M : Type u_1} [comm_monoid M] (f : ℕ → ℕ → M) {n : ℕ} :
∏ (i : ℕ × ℕ) in n.divisors_antidiagonal, f i.fst i.snd = ∏ (i : ℕ) in n.divisors, f (n / i) i
source
theorem nat.sum_divisors_antidiagonal' {M : Type u_1} [add_comm_monoid M] (f : ℕ → ℕ → M) {n : ℕ} :
∑ (i : ℕ × ℕ) in n.divisors_antidiagonal, f i.fst i.snd = ∑ (i : ℕ) in n.divisors, f (n / i) i
source
@[simp]
theorem nat.filter_dvd_eq_divisors {n : ℕ} (h : n ≠ 0) :
finset.filter (λ (x : ℕ), x ∣ n) (finset.range n.succ) = n.divisors
source
theorem nat.prime_divisors_eq_to_filter_divisors_prime (n : ℕ) :
n.factors.to_finset = finset.filter nat.prime n.divisors

The factors of n are the prime divisors

source
@[simp]
theorem nat.image_div_divisors_eq_divisors (n : ℕ) :
finset.image (λ (x : ℕ), n / x) n.divisors = n.divisors
source
@[simp]
theorem nat.sum_div_divisors {α : Type u_1} [add_comm_monoid α] (n : ℕ) (f : ℕ → α) :
∑ (d : ℕ) in n.divisors, f (n / d) = n.divisors.sum f
source
@[simp]
theorem nat.prod_div_divisors {α : Type u_1} [comm_monoid α] (n : ℕ) (f : ℕ → α) :
∏ (d : ℕ) in n.divisors, f (n / d) = n.divisors.prod f