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 thefinset
of natural numbers that dividen
.proper_divisors n
is thefinset
of natural numbers that dividen
, other thann
.divisors_antidiagonal n
is thefinset
of pairs(x,y)
such thatx * y = n
.perfect n
is true whenn
is positive and the sum ofproper_divisors n
isn
.
Implementation details #
divisors 0
,proper_divisors 0
, anddivisors_antidiagonal 0
are defined to be∅
.
Tags #
divisors, perfect numbers
divisors n
is the finset
of divisors of n
. As a special case, divisors 0 = ∅
.
Equations
- n.divisors = finset.filter (λ (x : ℕ), x ∣ n) (finset.Ico 1 (n + 1))
proper_divisors n
is the finset
of divisors of n
, other than n
.
As a special case, proper_divisors 0 = ∅
.
Equations
- n.proper_divisors = finset.filter (λ (x : ℕ), x ∣ n) (finset.Ico 1 n)
divisors_antidiagonal n
is the finset
of pairs (x,y)
such that x * y = n
.
As a special case, divisors_antidiagonal 0 = ∅
.
Equations
- n.divisors_antidiagonal = finset.filter (λ (x : ℕ × ℕ), x.fst * x.snd = n) (finset.Ico 1 (n + 1) ×ˢ finset.Ico 1 (n + 1))
@[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) :
finset.filter (λ (_x : ℕ), _x ∣ n) (finset.range n) = n.proper_divisors
theorem
nat.divisors_subset_proper_divisors
{n m : ℕ}
(hzero : n ≠ 0)
(h : m ∣ n)
(hdiff : m ≠ n) :
m.divisors ⊆ n.proper_divisors
@[simp]
theorem
nat.map_swap_divisors_antidiagonal
{n : ℕ} :
finset.map {to_fun := prod.swap ℕ, inj' := _} n.divisors_antidiagonal = n.divisors_antidiagonal
theorem
nat.divisors_prime_pow
{p : ℕ}
(pp : nat.prime p)
(k : ℕ) :
(p ^ k).divisors = finset.map {to_fun := has_pow.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) :
s.sum (λ (x : ℕ), x) = n.proper_divisors.sum (λ (x : ℕ), x) → s = n.proper_divisors
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}
[add_comm_monoid α]
{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
theorem
nat.proper_divisors_eq_singleton_one_iff_prime
{n : ℕ} :
n.proper_divisors = {1} ↔ nat.prime n
theorem
nat.proper_divisors_prime_pow
{p : ℕ}
(pp : nat.prime p)
(k : ℕ) :
(p ^ k).proper_divisors = finset.map {to_fun := has_pow.pow p, inj' := _} (finset.range k)
@[simp]
theorem
nat.sum_proper_divisors_prime_nsmul
{α : Type u_1}
[add_comm_monoid α]
{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))
The factors of n
are the prime divisors
@[simp]