# 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:

• divisors n is the Finset of natural numbers that divide n.
• properDivisors n is the Finset of natural numbers that divide n, other than n.
• divisorsAntidiagonal 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 properDivisors n is n.

## Implementation details #

• divisors 0, properDivisors 0, and divisorsAntidiagonal 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
Instances For

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

Equations
Instances For

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

Equations
Instances For
@[simp]
theorem Nat.filter_dvd_eq_divisors {n : } (h : n 0) :
Finset.filter (fun (x : ) => x n) (Finset.range n.succ) = n.divisors
@[simp]
theorem Nat.filter_dvd_eq_properDivisors {n : } (h : n 0) :
Finset.filter (fun (x : ) => x n) () = n.properDivisors
theorem Nat.properDivisors.not_self_mem {n : } :
nn.properDivisors
@[simp]
theorem Nat.mem_properDivisors {n : } {m : } :
n m.properDivisors n m n < m
theorem Nat.insert_self_properDivisors {n : } (h : n 0) :
insert n n.properDivisors = n.divisors
theorem Nat.cons_self_properDivisors {n : } (h : n 0) :
Finset.cons n n.properDivisors = n.divisors
@[simp]
theorem Nat.mem_divisors {n : } {m : } :
n m.divisors n m m 0
theorem Nat.one_mem_divisors {n : } :
1 n.divisors n 0
theorem Nat.mem_divisors_self (n : ) (h : n 0) :
n n.divisors
theorem Nat.dvd_of_mem_divisors {n : } {m : } (h : n m.divisors) :
n m
@[simp]
theorem Nat.mem_divisorsAntidiagonal {n : } {x : } :
x n.divisorsAntidiagonal x.1 * x.2 = n n 0
theorem Nat.ne_zero_of_mem_divisorsAntidiagonal {n : } {p : } (hp : p n.divisorsAntidiagonal) :
p.1 0 p.2 0
theorem Nat.left_ne_zero_of_mem_divisorsAntidiagonal {n : } {p : } (hp : p n.divisorsAntidiagonal) :
p.1 0
theorem Nat.right_ne_zero_of_mem_divisorsAntidiagonal {n : } {p : } (hp : p n.divisorsAntidiagonal) :
p.2 0
theorem Nat.divisor_le {n : } {m : } :
n m.divisorsn m
theorem Nat.divisors_subset_of_dvd {n : } {m : } (hzero : n 0) (h : m n) :
m.divisors n.divisors
theorem Nat.divisors_subset_properDivisors {n : } {m : } (hzero : n 0) (h : m n) (hdiff : m n) :
m.divisors n.properDivisors
theorem Nat.divisors_filter_dvd_of_dvd {n : } {m : } (hn : n 0) (hm : m n) :
Finset.filter (fun (x : ) => x m) n.divisors = m.divisors
@[simp]
@[simp]
theorem Nat.nonempty_divisors {n : } :
n.divisors.Nonempty n 0
@[simp]
theorem Nat.divisors_eq_empty {n : } :
n.divisors = n = 0
theorem Nat.properDivisors_subset_divisors {n : } :
n.properDivisors n.divisors
@[simp]
theorem Nat.divisors_one :
= {1}
theorem Nat.pos_of_mem_divisors {n : } {m : } (h : m n.divisors) :
0 < m
theorem Nat.pos_of_mem_properDivisors {n : } {m : } (h : m n.properDivisors) :
0 < m
theorem Nat.one_mem_properDivisors_iff_one_lt {n : } :
1 n.properDivisors 1 < n
@[simp]
theorem Nat.sup_divisors_id (n : ) :
n.divisors.sup id = n
theorem Nat.one_lt_of_mem_properDivisors {m : } {n : } (h : m n.properDivisors) :
1 < n
theorem Nat.one_lt_div_of_mem_properDivisors {m : } {n : } (h : m n.properDivisors) :
1 < n / m
theorem Nat.mem_properDivisors_iff_exists {m : } {n : } (hn : n 0) :
m n.properDivisors k > 1, n = m * k

See also Nat.mem_properDivisors.

@[simp]
theorem Nat.nonempty_properDivisors {n : } :
n.properDivisors.Nonempty 1 < n
@[simp]
theorem Nat.properDivisors_eq_empty {n : } :
n.properDivisors = n 1
@[simp]
@[simp]
theorem Nat.divisorsAntidiagonal_one :
= {(1, 1)}
theorem Nat.swap_mem_divisorsAntidiagonal {n : } {x : } :
x.swap n.divisorsAntidiagonal x n.divisorsAntidiagonal
@[simp]
theorem Nat.swap_mem_divisorsAntidiagonal_aux {n : } {x : } :
x.2 * x.1 = n ¬n = 0 x n.divisorsAntidiagonal
theorem Nat.fst_mem_divisors_of_mem_antidiagonal {n : } {x : } (h : x n.divisorsAntidiagonal) :
x.1 n.divisors
theorem Nat.snd_mem_divisors_of_mem_antidiagonal {n : } {x : } (h : x n.divisorsAntidiagonal) :
x.2 n.divisors
@[simp]
theorem Nat.map_swap_divisorsAntidiagonal {n : } :
Finset.map ().toEmbedding n.divisorsAntidiagonal = n.divisorsAntidiagonal
@[simp]
theorem Nat.image_fst_divisorsAntidiagonal {n : } :
Finset.image Prod.fst n.divisorsAntidiagonal = n.divisors
@[simp]
theorem Nat.image_snd_divisorsAntidiagonal {n : } :
Finset.image Prod.snd n.divisorsAntidiagonal = n.divisors
theorem Nat.map_div_right_divisors {n : } :
Finset.map { toFun := fun (d : ) => (d, n / d), inj' := } n.divisors = n.divisorsAntidiagonal
theorem Nat.map_div_left_divisors {n : } :
Finset.map { toFun := fun (d : ) => (n / d, d), inj' := } n.divisors = n.divisorsAntidiagonal
theorem Nat.sum_divisors_eq_sum_properDivisors_add_self {n : } :
(n.divisors.sum fun (i : ) => i) = (n.properDivisors.sum fun (i : ) => i) + n
def Nat.Perfect (n : ) :

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

Equations
• n.Perfect = ((n.properDivisors.sum fun (i : ) => i) = n 0 < n)
Instances For
theorem Nat.perfect_iff_sum_properDivisors {n : } (h : 0 < n) :
n.Perfect (n.properDivisors.sum fun (i : ) => i) = n
theorem Nat.perfect_iff_sum_divisors_eq_two_mul {n : } (h : 0 < n) :
n.Perfect (n.divisors.sum fun (i : ) => i) = 2 * n
theorem Nat.mem_divisors_prime_pow {p : } (pp : p.Prime) (k : ) {x : } :
x (p ^ k).divisors jk, x = p ^ j
theorem Nat.Prime.divisors {p : } (pp : p.Prime) :
p.divisors = {1, p}
theorem Nat.Prime.properDivisors {p : } (pp : p.Prime) :
p.properDivisors = {1}
theorem Nat.divisors_prime_pow {p : } (pp : p.Prime) (k : ) :
(p ^ k).divisors = Finset.map { toFun := fun (x : ) => p ^ x, inj' := } (Finset.range (k + 1))
@[simp]
theorem Nat.divisors_inj {a : } {b : } :
a.divisors = b.divisors a = b
theorem Nat.eq_properDivisors_of_subset_of_sum_eq_sum {n : } {s : } (hsub : s n.properDivisors) :
((s.sum fun (x : ) => x) = n.properDivisors.sum fun (x : ) => x)s = n.properDivisors
theorem Nat.sum_properDivisors_dvd {n : } (h : (n.properDivisors.sum fun (x : ) => x) n) :
(n.properDivisors.sum fun (x : ) => x) = 1 (n.properDivisors.sum fun (x : ) => x) = n
@[simp]
theorem Nat.Prime.sum_properDivisors {α : Type u_1} [] {p : } {f : α} (h : p.Prime) :
(p.properDivisors.sum fun (x : ) => f x) = f 1
@[simp]
theorem Nat.Prime.prod_properDivisors {α : Type u_1} [] {p : } {f : α} (h : p.Prime) :
(p.properDivisors.prod fun (x : ) => f x) = f 1
@[simp]
theorem Nat.Prime.sum_divisors {α : Type u_1} [] {p : } {f : α} (h : p.Prime) :
(p.divisors.sum fun (x : ) => f x) = f p + f 1
@[simp]
theorem Nat.Prime.prod_divisors {α : Type u_1} [] {p : } {f : α} (h : p.Prime) :
(p.divisors.prod fun (x : ) => f x) = f p * f 1
theorem Nat.properDivisors_eq_singleton_one_iff_prime {n : } :
n.properDivisors = {1} n.Prime
theorem Nat.sum_properDivisors_eq_one_iff_prime {n : } :
(n.properDivisors.sum fun (x : ) => x) = 1 n.Prime
theorem Nat.mem_properDivisors_prime_pow {p : } (pp : p.Prime) (k : ) {x : } :
x (p ^ k).properDivisors ∃ (j : ) (_ : j < k), x = p ^ j
theorem Nat.properDivisors_prime_pow {p : } (pp : p.Prime) (k : ) :
(p ^ k).properDivisors = Finset.map { toFun := fun (x : ) => p ^ x, inj' := } ()
@[simp]
theorem Nat.sum_properDivisors_prime_nsmul {α : Type u_1} [] {k : } {p : } {f : α} (h : p.Prime) :
((p ^ k).properDivisors.sum fun (x : ) => f x) = ().sum fun (x : ) => f (p ^ x)
@[simp]
theorem Nat.prod_properDivisors_prime_pow {α : Type u_1} [] {k : } {p : } {f : α} (h : p.Prime) :
((p ^ k).properDivisors.prod fun (x : ) => f x) = ().prod fun (x : ) => f (p ^ x)
@[simp]
theorem Nat.sum_divisors_prime_pow {α : Type u_1} [] {k : } {p : } {f : α} (h : p.Prime) :
((p ^ k).divisors.sum fun (x : ) => f x) = (Finset.range (k + 1)).sum fun (x : ) => f (p ^ x)
@[simp]
theorem Nat.prod_divisors_prime_pow {α : Type u_1} [] {k : } {p : } {f : α} (h : p.Prime) :
((p ^ k).divisors.prod fun (x : ) => f x) = (Finset.range (k + 1)).prod fun (x : ) => f (p ^ x)
theorem Nat.sum_divisorsAntidiagonal {M : Type u_1} [] (f : M) {n : } :
(n.divisorsAntidiagonal.sum fun (i : ) => f i.1 i.2) = n.divisors.sum fun (i : ) => f i (n / i)
theorem Nat.prod_divisorsAntidiagonal {M : Type u_1} [] (f : M) {n : } :
(n.divisorsAntidiagonal.prod fun (i : ) => f i.1 i.2) = n.divisors.prod fun (i : ) => f i (n / i)
theorem Nat.sum_divisorsAntidiagonal' {M : Type u_1} [] (f : M) {n : } :
(n.divisorsAntidiagonal.sum fun (i : ) => f i.1 i.2) = n.divisors.sum fun (i : ) => f (n / i) i
theorem Nat.prod_divisorsAntidiagonal' {M : Type u_1} [] (f : M) {n : } :
(n.divisorsAntidiagonal.prod fun (i : ) => f i.1 i.2) = n.divisors.prod fun (i : ) => f (n / i) i
theorem Nat.prime_divisors_eq_to_filter_divisors_prime (n : ) :
n.factors.toFinset = Finset.filter Nat.Prime n.divisors

The factors of n are the prime divisors

theorem Nat.prime_divisors_filter_dvd_of_dvd {m : } {n : } (hn : n 0) (hmn : m n) :
Finset.filter (fun (x : ) => x m) n.factors.toFinset = m.factors.toFinset
@[simp]
theorem Nat.image_div_divisors_eq_divisors (n : ) :
Finset.image (fun (x : ) => n / x) n.divisors = n.divisors
theorem Nat.sum_div_divisors {α : Type u_1} [] (n : ) (f : α) :
(n.divisors.sum fun (d : ) => f (n / d)) = n.divisors.sum f
theorem Nat.prod_div_divisors {α : Type u_1} [] (n : ) (f : α) :
(n.divisors.prod fun (d : ) => f (n / d)) = n.divisors.prod f