Documentation

Mathlib.NumberTheory.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
ink
def Nat.divisors (n : ℕ) :
Finset ℕ

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

Equations
source
ink
def Nat.properDivisors (n : ℕ) :
Finset ℕ

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

Equations
source
ink
def Nat.divisorsAntidiagonal (n : ℕ) :
Finset (ℕ × ℕ)

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

Equations
source
ink
@[simp]
theorem Nat.filter_dvd_eq_divisors {n : ℕ} (h : n ≠ 0) :
Finset.filter (fun x => x ∣ n) (Finset.range (Nat.succ n)) = Nat.divisors n
source
ink
@[simp]
theorem Nat.filter_dvd_eq_properDivisors {n : ℕ} (h : n ≠ 0) :
Finset.filter (fun x => x ∣ n) (Finset.range n) = Nat.properDivisors n
source
ink
theorem Nat.properDivisors.not_self_mem {n : ℕ} :
¬n ∈ Nat.properDivisors n
source
ink
@[simp]
theorem Nat.mem_properDivisors {n : ℕ} {m : ℕ} :
n ∈ Nat.properDivisors m ↔ n ∣ m ∧ n < m
source
ink
theorem Nat.insert_self_properDivisors {n : ℕ} (h : n ≠ 0) :
insert n (Nat.properDivisors n) = Nat.divisors n
source
ink
theorem Nat.cons_self_properDivisors {n : ℕ} (h : n ≠ 0) :
Finset.cons n (Nat.properDivisors n) (_ : ¬n ∈ Nat.properDivisors n) = Nat.divisors n
source
ink
@[simp]
theorem Nat.mem_divisors {n : ℕ} {m : ℕ} :
n ∈ Nat.divisors m ↔ n ∣ m ∧ m ≠ 0
source
ink
theorem Nat.one_mem_divisors {n : ℕ} :
1 ∈ Nat.divisors n ↔ n ≠ 0
source
ink
theorem Nat.mem_divisors_self (n : ℕ) (h : n ≠ 0) :
n ∈ Nat.divisors n
source
ink
theorem Nat.dvd_of_mem_divisors {n : ℕ} {m : ℕ} (h : n ∈ Nat.divisors m) :
n ∣ m
source
ink
@[simp]
theorem Nat.mem_divisorsAntidiagonal {n : ℕ} {x : ℕ × ℕ} :
x ∈ Nat.divisorsAntidiagonal n ↔ x.fst * x.snd = n ∧ n ≠ 0
source
ink
theorem Nat.divisor_le {n : ℕ} {m : ℕ} :
n ∈ Nat.divisors m → n ≤ m
source
ink
theorem Nat.divisors_subset_of_dvd {n : ℕ} {m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) :
Nat.divisors m ⊆ Nat.divisors n
source
ink
theorem Nat.divisors_subset_properDivisors {n : ℕ} {m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) (hdiff : m ≠ n) :
Nat.divisors m ⊆ Nat.properDivisors n
source
ink
@[simp]
theorem Nat.divisors_zero :
Nat.divisors 0 = ∅
source
ink
@[simp]
theorem Nat.properDivisors_zero :
Nat.properDivisors 0 = ∅
source
ink
theorem Nat.properDivisors_subset_divisors {n : ℕ} :
Nat.properDivisors n ⊆ Nat.divisors n
source
ink
@[simp]
theorem Nat.divisors_one :
Nat.divisors 1 = {1}
source
ink
@[simp]
theorem Nat.properDivisors_one :
Nat.properDivisors 1 = ∅
source
ink
theorem Nat.pos_of_mem_divisors {n : ℕ} {m : ℕ} (h : m ∈ Nat.divisors n) :
0 < m
source
ink
theorem Nat.pos_of_mem_properDivisors {n : ℕ} {m : ℕ} (h : m ∈ Nat.properDivisors n) :
0 < m
source
ink
theorem Nat.one_mem_properDivisors_iff_one_lt {n : ℕ} :
1 ∈ Nat.properDivisors n ↔ 1 < n
source
ink
@[simp]
theorem Nat.divisorsAntidiagonal_zero :
Nat.divisorsAntidiagonal 0 = ∅
source
ink
@[simp]
theorem Nat.divisorsAntidiagonal_one :
Nat.divisorsAntidiagonal 1 = {(1, 1)}
source
ink
theorem Nat.swap_mem_divisorsAntidiagonal {n : ℕ} {x : ℕ × ℕ} :
Prod.swap x ∈ Nat.divisorsAntidiagonal n ↔ x ∈ Nat.divisorsAntidiagonal n
source
ink
@[simp]
theorem Nat.swap_mem_divisorsAntidiagonal_aux {n : ℕ} {x : ℕ × ℕ} :
x.snd * x.fst = n ∧ ¬n = 0 ↔ x ∈ Nat.divisorsAntidiagonal n
source
ink
theorem Nat.fst_mem_divisors_of_mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} (h : x ∈ Nat.divisorsAntidiagonal n) :
x.fst ∈ Nat.divisors n
source
ink
theorem Nat.snd_mem_divisors_of_mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} (h : x ∈ Nat.divisorsAntidiagonal n) :
x.snd ∈ Nat.divisors n
source
ink
@[simp]
theorem Nat.map_swap_divisorsAntidiagonal {n : ℕ} :
Finset.map (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) (Nat.divisorsAntidiagonal n) = Nat.divisorsAntidiagonal n
source
ink
@[simp]
theorem Nat.image_fst_divisorsAntidiagonal {n : ℕ} :
Finset.image Prod.fst (Nat.divisorsAntidiagonal n) = Nat.divisors n
source
ink
@[simp]
theorem Nat.image_snd_divisorsAntidiagonal {n : ℕ} :
Finset.image Prod.snd (Nat.divisorsAntidiagonal n) = Nat.divisors n
source
ink
theorem Nat.map_div_right_divisors {n : ℕ} :
Finset.map { toFun := fun d => (d, n / d), inj' := (_ : ∀ (p₁ p₂ : ℕ), (fun d => (d, n / d)) p₁ = (fun d => (d, n / d)) p₂ → ((fun d => (d, n / d)) p₁).fst = ((fun d => (d, n / d)) p₂).fst) } (Nat.divisors n) = Nat.divisorsAntidiagonal n
source
ink
theorem Nat.map_div_left_divisors {n : ℕ} :
Finset.map { toFun := fun d => (n / d, d), inj' := (_ : ∀ (p₁ p₂ : ℕ), (fun d => (n / d, d)) p₁ = (fun d => (n / d, d)) p₂ → ((fun d => (n / d, d)) p₁).snd = ((fun d => (n / d, d)) p₂).snd) } (Nat.divisors n) = Nat.divisorsAntidiagonal n
source
ink
theorem Nat.sum_divisors_eq_sum_properDivisors_add_self {n : ℕ} :
(Finset.sum (Nat.divisors n) fun i => i) = (Finset.sum (Nat.properDivisors n) fun i => i) + n
source
ink
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
ink
theorem Nat.perfect_iff_sum_properDivisors {n : ℕ} (h : 0 < n) :
Nat.Perfect n ↔ (Finset.sum (Nat.properDivisors n) fun i => i) = n
source
ink
theorem Nat.perfect_iff_sum_divisors_eq_two_mul {n : ℕ} (h : 0 < n) :
Nat.Perfect n ↔ (Finset.sum (Nat.divisors n) fun i => i) = 2 * n
source
ink
theorem Nat.mem_divisors_prime_pow {p : ℕ} (pp : Nat.Prime p) (k : ℕ) {x : ℕ} :
x ∈ Nat.divisors (p ^ k) ↔ ∃ j x, x = p ^ j
source
ink
theorem Nat.Prime.divisors {p : ℕ} (pp : Nat.Prime p) :
Nat.divisors p = {1, p}
source
ink
theorem Nat.Prime.properDivisors {p : ℕ} (pp : Nat.Prime p) :
Nat.properDivisors p = {1}
source
ink
theorem Nat.divisors_prime_pow {p : ℕ} (pp : Nat.Prime p) (k : ℕ) :
Nat.divisors (p ^ k) = Finset.map { toFun := Nat.pow p, inj' := (_ : Function.Injective fun n => p ^ n) } (Finset.range (k + 1))
source
ink
theorem Nat.eq_properDivisors_of_subset_of_sum_eq_sum {n : ℕ} {s : Finset ℕ} (hsub : s ⊆ Nat.properDivisors n) :
((Finset.sum s fun x => x) = Finset.sum (Nat.properDivisors n) fun x => x) → s = Nat.properDivisors n
source
ink
theorem Nat.sum_properDivisors_dvd {n : ℕ} (h : (Finset.sum (Nat.properDivisors n) fun x => x) ∣ n) :
(Finset.sum (Nat.properDivisors n) fun x => x) = 1 ∨ (Finset.sum (Nat.properDivisors n) fun x => x) = n
source
ink
@[simp]
theorem Nat.Prime.sum_properDivisors {α : Type u_1} [inst : AddCommMonoid α] {p : ℕ} {f : ℕ → α} (h : Nat.Prime p) :
(Finset.sum (Nat.properDivisors p) fun x => f x) = f 1
source
ink
@[simp]
theorem Nat.Prime.prod_properDivisors {α : Type u_1} [inst : CommMonoid α] {p : ℕ} {f : ℕ → α} (h : Nat.Prime p) :
(Finset.prod (Nat.properDivisors p) fun x => f x) = f 1
source
ink
@[simp]
theorem Nat.Prime.sum_divisors {α : Type u_1} [inst : AddCommMonoid α] {p : ℕ} {f : ℕ → α} (h : Nat.Prime p) :
(Finset.sum (Nat.divisors p) fun x => f x) = f p + f 1
source
ink
@[simp]
theorem Nat.Prime.prod_divisors {α : Type u_1} [inst : CommMonoid α] {p : ℕ} {f : ℕ → α} (h : Nat.Prime p) :
(Finset.prod (Nat.divisors p) fun x => f x) = f p * f 1
source
ink
theorem Nat.properDivisors_eq_singleton_one_iff_prime {n : ℕ} :
Nat.properDivisors n = {1} ↔ Nat.Prime n
source
ink
theorem Nat.sum_properDivisors_eq_one_iff_prime {n : ℕ} :
(Finset.sum (Nat.properDivisors n) fun x => x) = 1 ↔ Nat.Prime n
source
ink
theorem Nat.mem_properDivisors_prime_pow {p : ℕ} (pp : Nat.Prime p) (k : ℕ) {x : ℕ} :
x ∈ Nat.properDivisors (p ^ k) ↔ ∃ j x, x = p ^ j
source
ink
theorem Nat.properDivisors_prime_pow {p : ℕ} (pp : Nat.Prime p) (k : ℕ) :
Nat.properDivisors (p ^ k) = Finset.map { toFun := Nat.pow p, inj' := (_ : Function.Injective fun n => p ^ n) } (Finset.range k)
source
ink
@[simp]
theorem Nat.sum_properDivisors_prime_nsmul {α : Type u_1} [inst : AddCommMonoid α] {k : ℕ} {p : ℕ} {f : ℕ → α} (h : Nat.Prime p) :
(Finset.sum (Nat.properDivisors (p ^ k)) fun x => f x) = Finset.sum (Finset.range k) fun x => f (p ^ x)
source
ink
@[simp]
theorem Nat.prod_properDivisors_prime_pow {α : Type u_1} [inst : CommMonoid α] {k : ℕ} {p : ℕ} {f : ℕ → α} (h : Nat.Prime p) :
(Finset.prod (Nat.properDivisors (p ^ k)) fun x => f x) = Finset.prod (Finset.range k) fun x => f (p ^ x)
source
ink
@[simp]
theorem Nat.sum_divisors_prime_pow {α : Type u_1} [inst : AddCommMonoid α] {k : ℕ} {p : ℕ} {f : ℕ → α} (h : Nat.Prime p) :
(Finset.sum (Nat.divisors (p ^ k)) fun x => f x) = Finset.sum (Finset.range (k + 1)) fun x => f (p ^ x)
source
ink
@[simp]
theorem Nat.prod_divisors_prime_pow {α : Type u_1} [inst : CommMonoid α] {k : ℕ} {p : ℕ} {f : ℕ → α} (h : Nat.Prime p) :
(Finset.prod (Nat.divisors (p ^ k)) fun x => f x) = Finset.prod (Finset.range (k + 1)) fun x => f (p ^ x)
source
ink
theorem Nat.sum_divisorsAntidiagonal {M : Type u_1} [inst : AddCommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} :
(Finset.sum (Nat.divisorsAntidiagonal n) fun i => f i.fst i.snd) = Finset.sum (Nat.divisors n) fun i => f i (n / i)
source
ink
theorem Nat.prod_divisorsAntidiagonal {M : Type u_1} [inst : CommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} :
(Finset.prod (Nat.divisorsAntidiagonal n) fun i => f i.fst i.snd) = Finset.prod (Nat.divisors n) fun i => f i (n / i)
source
ink
theorem Nat.sum_divisorsAntidiagonal' {M : Type u_1} [inst : AddCommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} :
(Finset.sum (Nat.divisorsAntidiagonal n) fun i => f i.fst i.snd) = Finset.sum (Nat.divisors n) fun i => f (n / i) i
source
ink
theorem Nat.prod_divisorsAntidiagonal' {M : Type u_1} [inst : CommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} :
(Finset.prod (Nat.divisorsAntidiagonal n) fun i => f i.fst i.snd) = Finset.prod (Nat.divisors n) fun i => f (n / i) i
source
ink
theorem Nat.prime_divisors_eq_to_filter_divisors_prime (n : ℕ) :
List.toFinset (Nat.factors n) = Finset.filter Nat.Prime (Nat.divisors n)

The factors of n are the prime divisors

source
ink
@[simp]
theorem Nat.image_div_divisors_eq_divisors (n : ℕ) :
Finset.image (fun x => n / x) (Nat.divisors n) = Nat.divisors n
source
ink
theorem Nat.sum_div_divisors {α : Type u_1} [inst : AddCommMonoid α] (n : ℕ) (f : ℕ → α) :
(Finset.sum (Nat.divisors n) fun d => f (n / d)) = Finset.sum (Nat.divisors n) f
source
ink
theorem Nat.prod_div_divisors {α : Type u_1} [inst : CommMonoid α] (n : ℕ) (f : ℕ → α) :
(Finset.prod (Nat.divisors n) fun d => f (n / d)) = Finset.prod (Nat.divisors n) f