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

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

Equations

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

Equations

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

Equations
@[simp]
theorem Nat.filter_dvd_eq_divisors {n : } (h : n 0) :
@[simp]
theorem Nat.mem_properDivisors {n : } {m : } :
@[simp]
theorem Nat.mem_divisors {n : } {m : } :
theorem Nat.dvd_of_mem_divisors {n : } {m : } (h : n Nat.divisors m) :
n m
@[simp]
theorem Nat.mem_divisorsAntidiagonal {n : } {x : × } :
x Nat.divisorsAntidiagonal n x.fst * x.snd = n n 0
theorem Nat.divisor_le {n : } {m : } :
n Nat.divisors mn m
theorem Nat.divisors_subset_of_dvd {n : } {m : } (hzero : n 0) (h : m n) :
theorem Nat.divisors_subset_properDivisors {n : } {m : } (hzero : n 0) (h : m n) (hdiff : m n) :
theorem Nat.pos_of_mem_divisors {n : } {m : } (h : m Nat.divisors n) :
0 < m
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
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
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
theorem Nat.mem_divisors_prime_pow {p : } (pp : Nat.Prime p) (k : ) {x : } :
x Nat.divisors (p ^ k) j x, x = p ^ j
theorem Nat.Prime.divisors {p : } (pp : Nat.Prime p) :
Nat.divisors p = {1, p}
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))
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
@[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
@[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
@[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
@[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
theorem Nat.mem_properDivisors_prime_pow {p : } (pp : Nat.Prime p) (k : ) {x : } :
x Nat.properDivisors (p ^ k) j x, x = p ^ j
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)
@[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)
@[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)
@[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)
@[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)
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)
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)
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
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
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
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