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

def nat.divisors (n : ) :

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

Equations

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.mem_proper_divisors {n m : } :

@[simp]
theorem nat.mem_divisors {n m : } :
n m.divisors n m m 0

theorem nat.dvd_of_mem_divisors {n m : } (h : n m.divisors) :
n m

@[simp]
theorem nat.mem_divisors_antidiagonal {n : } {x : × } :

theorem nat.divisor_le {n m : } :
n m.divisorsn m

@[simp]

@[simp]
theorem nat.divisors_one  :
1.divisors = {1}

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

theorem nat.sum_divisors_eq_sum_proper_divisors_add_self {n : } :
∑ (i : ) in n.divisors, i = ∑ (i : ) in n.proper_divisors, 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 ∑ (i : ) in n.proper_divisors, i = n

theorem nat.perfect_iff_sum_divisors_eq_two_mul {n : } (h : 0 < n) :
n.perfect ∑ (i : ) in n.divisors, 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 := pow p, inj' := _} (finset.range (k + 1))

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, xs = n.proper_divisors

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

@[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

@[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

@[simp]
theorem nat.prod_divisors_prime {α : Type u_1} [comm_monoid α] {p : } {f : → α} (h : nat.prime p) :
∏ (x : ) in p.divisors, f x = (f p) * f 1

@[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)

@[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)

@[simp]
theorem nat.filter_dvd_eq_divisors {n : } (h : n 0) :