# mathlib3documentation

number_theory.divisors

# Divisor finsets #

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

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:

• divisors n is the finset of natural numbers that divide n.
• proper_divisors n is the finset of natural numbers that divide n, other than n.
• divisors_antidiagonal n is the finset of pairs (x,y) such that x * y = n.
• perfect n is true when n is positive and the sum of proper_divisors n is n.

## Implementation details #

• divisors 0, proper_divisors 0, and divisors_antidiagonal 0 are defined to be ∅.

## Tags #

divisors, perfect numbers

def nat.divisors (n : ) :

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

Equations
def nat.proper_divisors (n : ) :

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

Equations

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

Equations
@[simp]
theorem nat.filter_dvd_eq_divisors {n : } (h : n 0) :
finset.filter (λ (_x : ), _x n) (finset.range n.succ) = n.divisors
@[simp]
theorem nat.filter_dvd_eq_proper_divisors {n : } (h : n 0) :
@[simp]
theorem nat.mem_proper_divisors {n m : } :
n m n < m
theorem nat.insert_self_proper_divisors {n : } (h : n 0) :
theorem nat.cons_self_proper_divisors {n : } (h : n 0) :
@[simp]
theorem nat.mem_divisors {n m : } :
n m.divisors n m m 0
theorem nat.one_mem_divisors {n : } :
theorem nat.mem_divisors_self (n : ) (h : n 0) :
theorem nat.dvd_of_mem_divisors {n m : } (h : n m.divisors) :
n m
@[simp]
theorem nat.mem_divisors_antidiagonal {n : } {x : × } :
x.fst * x.snd = n n 0
theorem nat.divisor_le {n m : } :
theorem nat.divisors_subset_of_dvd {n m : } (hzero : n 0) (h : m n) :
theorem nat.divisors_subset_proper_divisors {n m : } (hzero : n 0) (h : m n) (hdiff : m n) :
@[simp]
theorem nat.divisors_zero  :
@[simp]
@[simp]
theorem nat.divisors_one  :
1.divisors = {1}
@[simp]
theorem nat.pos_of_mem_divisors {n m : } (h : m n.divisors) :
0 < m
theorem nat.pos_of_mem_proper_divisors {n m : } (h : m n.proper_divisors) :
0 < m
@[simp]
@[simp]
@[simp]
theorem nat.map_div_right_divisors {n : } :
finset.map {to_fun := λ (d : ), (d, n / d), inj' := _} n.divisors = n.divisors_antidiagonal
theorem nat.map_div_left_divisors {n : } :
finset.map {to_fun := λ (d : ), (n / d, d), inj' := _} n.divisors = n.divisors_antidiagonal
theorem nat.sum_divisors_eq_sum_proper_divisors_add_self {n : } :
n.divisors.sum (λ (i : ), i) = n.proper_divisors.sum (λ (i : ), i) + n
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
theorem nat.perfect_iff_sum_proper_divisors {n : } (h : 0 < n) :
n.perfect n.proper_divisors.sum (λ (i : ), i) = n
theorem nat.perfect_iff_sum_divisors_eq_two_mul {n : } (h : 0 < n) :
n.perfect n.divisors.sum (λ (i : ), i) = 2 * n
theorem nat.mem_divisors_prime_pow {p : } (pp : nat.prime p) (k : ) {x : } :
x (p ^ k).divisors (j : ) (H : j k), x = p ^ j
theorem nat.prime.divisors {p : } (pp : nat.prime p) :
p.divisors = {1, p}
theorem nat.divisors_prime_pow {p : } (pp : nat.prime p) (k : ) :
(p ^ k).divisors = finset.map {to_fun := , inj' := _} (finset.range (k + 1))
theorem nat.eq_proper_divisors_of_subset_of_sum_eq_sum {n : } {s : finset } (hsub : s n.proper_divisors) :
s.sum (λ (x : ), x) = n.proper_divisors.sum (λ (x : ), x)
theorem nat.sum_proper_divisors_dvd {n : } (h : n.proper_divisors.sum (λ (x : ), x) n) :
n.proper_divisors.sum (λ (x : ), x) = 1 n.proper_divisors.sum (λ (x : ), x) = n
@[simp]
theorem nat.prime.sum_proper_divisors {α : Type u_1} {p : } {f : α} (h : nat.prime p) :
p.proper_divisors.sum (λ (x : ), f x) = f 1
@[simp]
theorem nat.prime.prod_proper_divisors {α : Type u_1} [comm_monoid α] {p : } {f : α} (h : nat.prime p) :
p.proper_divisors.prod (λ (x : ), f x) = f 1
@[simp]
theorem nat.prime.sum_divisors {α : Type u_1} {p : } {f : α} (h : nat.prime p) :
p.divisors.sum (λ (x : ), f x) = f p + f 1
@[simp]
theorem nat.prime.prod_divisors {α : Type u_1} [comm_monoid α] {p : } {f : α} (h : nat.prime p) :
p.divisors.prod (λ (x : ), f x) = f p * f 1
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
@[simp]
theorem nat.sum_proper_divisors_prime_nsmul {α : Type u_1} {k p : } {f : α} (h : nat.prime p) :
(p ^ k).proper_divisors.sum (λ (x : ), f x) = (finset.range k).sum (λ (x : ), f (p ^ x))
@[simp]
theorem nat.prod_proper_divisors_prime_pow {α : Type u_1} [comm_monoid α] {k p : } {f : α} (h : nat.prime p) :
(p ^ k).proper_divisors.prod (λ (x : ), f x) = (finset.range k).prod (λ (x : ), f (p ^ x))
@[simp]
theorem nat.sum_divisors_prime_pow {α : Type u_1} {k p : } {f : α} (h : nat.prime p) :
(p ^ k).divisors.sum (λ (x : ), f x) = (finset.range (k + 1)).sum (λ (x : ), f (p ^ x))
@[simp]
theorem nat.prod_divisors_prime_pow {α : Type u_1} [comm_monoid α] {k p : } {f : α} (h : nat.prime p) :
(p ^ k).divisors.prod (λ (x : ), f x) = (finset.range (k + 1)).prod (λ (x : ), f (p ^ x))
theorem nat.prod_divisors_antidiagonal {M : Type u_1} [comm_monoid M] (f : M) {n : } :
n.divisors_antidiagonal.prod (λ (i : × ), f i.fst i.snd) = n.divisors.prod (λ (i : ), f i (n / i))
theorem nat.sum_divisors_antidiagonal {M : Type u_1} (f : M) {n : } :
n.divisors_antidiagonal.sum (λ (i : × ), f i.fst i.snd) = n.divisors.sum (λ (i : ), f i (n / i))
theorem nat.prod_divisors_antidiagonal' {M : Type u_1} [comm_monoid M] (f : M) {n : } :
n.divisors_antidiagonal.prod (λ (i : × ), f i.fst i.snd) = n.divisors.prod (λ (i : ), f (n / i) i)
theorem nat.sum_divisors_antidiagonal' {M : Type u_1} (f : M) {n : } :
n.divisors_antidiagonal.sum (λ (i : × ), f i.fst i.snd) = n.divisors.sum (λ (i : ), f (n / i) i)

The factors of n are the prime divisors

@[simp]
@[simp]
theorem nat.sum_div_divisors {α : Type u_1} (n : ) (f : α) :
n.divisors.sum (λ (d : ), f (n / d)) = n.divisors.sum f
@[simp]
theorem nat.prod_div_divisors {α : Type u_1} [comm_monoid α] (n : ) (f : α) :
n.divisors.prod (λ (d : ), f (n / d)) = n.divisors.prod f