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 : ℕ) : Finset ℕ

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

Equations

• Nat.divisors n = Finset.filter (fun (x : ℕ) => x ∣ n) (Finset.Ico 1 (n + 1))

def Nat.properDivisors (n : ℕ) : Finset ℕ

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

Equations

• Nat.properDivisors n = Finset.filter (fun (x : ℕ) => x ∣ n) (Finset.Ico 1 n)

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

• Nat.divisorsAntidiagonal n = Finset.filter (fun (x : ℕ × ℕ) => x.1 * x.2 = n) (Finset.Ico 1 (n + 1) ×ˢ Finset.Ico 1 (n + 1))

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

@[simp]

theorem Nat.filter_dvd_eq_properDivisors {n : ℕ} (h : n ≠ 0) : Finset.filter (fun (x : ℕ) => x ∣ n) (Finset.range n) = Nat.properDivisors n

theorem Nat.properDivisors.not_self_mem {n : ℕ} : n ∉ Nat.properDivisors n

@[simp]

theorem Nat.mem_properDivisors {n : ℕ} {m : ℕ} : n ∈ Nat.properDivisors m ↔ n ∣ m ∧ n < m

theorem Nat.insert_self_properDivisors {n : ℕ} (h : n ≠ 0) : insert n (Nat.properDivisors n) = Nat.divisors n

theorem Nat.cons_self_properDivisors {n : ℕ} (h : n ≠ 0) : Finset.cons n (Nat.properDivisors n) (_ : n ∉ Nat.properDivisors n) = Nat.divisors n

@[simp]

theorem Nat.mem_divisors {n : ℕ} {m : ℕ} : n ∈ Nat.divisors m ↔ n ∣ m ∧ m ≠ 0

theorem Nat.one_mem_divisors {n : ℕ} : 1 ∈ Nat.divisors n ↔ n ≠ 0

theorem Nat.mem_divisors_self (n : ℕ) (h : n ≠ 0) : n ∈ Nat.divisors n

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.1 * x.2 = n ∧ n ≠ 0

theorem Nat.divisor_le {n : ℕ} {m : ℕ} : n ∈ Nat.divisors m → n ≤ m

theorem Nat.divisors_subset_of_dvd {n : ℕ} {m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) : Nat.divisors m ⊆ Nat.divisors n

theorem Nat.divisors_subset_properDivisors {n : ℕ} {m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) (hdiff : m ≠ n) : Nat.divisors m ⊆ Nat.properDivisors n

theorem Nat.divisors_filter_dvd_of_dvd {n : ℕ} {m : ℕ} (hn : n ≠ 0) (hm : m ∣ n) : Finset.filter (fun (x : ℕ) => x ∣ m) (Nat.divisors n) = Nat.divisors m

@[simp]

theorem Nat.divisors_zero : Nat.divisors 0 = ∅

@[simp]

theorem Nat.properDivisors_zero : Nat.properDivisors 0 = ∅

@[simp]

theorem Nat.nonempty_divisors {n : ℕ} : (Nat.divisors n).Nonempty ↔ n ≠ 0

@[simp]

theorem Nat.divisors_eq_empty {n : ℕ} : Nat.divisors n = ∅ ↔ n = 0

theorem Nat.properDivisors_subset_divisors {n : ℕ} : Nat.properDivisors n ⊆ Nat.divisors n

@[simp]

theorem Nat.divisors_one : Nat.divisors 1 = {1}

@[simp]

theorem Nat.properDivisors_one : Nat.properDivisors 1 = ∅

theorem Nat.pos_of_mem_divisors {n : ℕ} {m : ℕ} (h : m ∈ Nat.divisors n) : 0 < m

theorem Nat.pos_of_mem_properDivisors {n : ℕ} {m : ℕ} (h : m ∈ Nat.properDivisors n) : 0 < m

theorem Nat.one_mem_properDivisors_iff_one_lt {n : ℕ} : 1 ∈ Nat.properDivisors n ↔ 1 < n

@[simp]

theorem Nat.sup_divisors_id (n : ℕ) : Finset.sup (Nat.divisors n) id = n

theorem Nat.one_lt_of_mem_properDivisors {m : ℕ} {n : ℕ} (h : m ∈ Nat.properDivisors n) : 1 < n

theorem Nat.one_lt_div_of_mem_properDivisors {m : ℕ} {n : ℕ} (h : m ∈ Nat.properDivisors n) : 1 < n / m

theorem Nat.mem_properDivisors_iff_exists {m : ℕ} {n : ℕ} (hn : n ≠ 0) : m ∈ Nat.properDivisors n ↔ ∃ k > 1, n = m * k

See also Nat.mem_properDivisors.

@[simp]

theorem Nat.nonempty_properDivisors {n : ℕ} : (Nat.properDivisors n).Nonempty ↔ 1 < n

@[simp]

theorem Nat.properDivisors_eq_empty {n : ℕ} : Nat.properDivisors n = ∅ ↔ n ≤ 1

@[simp]

theorem Nat.divisorsAntidiagonal_zero : Nat.divisorsAntidiagonal 0 = ∅

@[simp]

theorem Nat.divisorsAntidiagonal_one : Nat.divisorsAntidiagonal 1 = {(1, 1)}

theorem Nat.swap_mem_divisorsAntidiagonal {n : ℕ} {x : ℕ × ℕ} : Prod.swap x ∈ Nat.divisorsAntidiagonal n ↔ x ∈ Nat.divisorsAntidiagonal n

@[simp]

theorem Nat.swap_mem_divisorsAntidiagonal_aux {n : ℕ} {x : ℕ × ℕ} : x.2 * x.1 = n ∧ ¬n = 0 ↔ x ∈ Nat.divisorsAntidiagonal n

theorem Nat.fst_mem_divisors_of_mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} (h : x ∈ Nat.divisorsAntidiagonal n) : x.1 ∈ Nat.divisors n

theorem Nat.snd_mem_divisors_of_mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} (h : x ∈ Nat.divisorsAntidiagonal n) : x.2 ∈ Nat.divisors n

@[simp]

theorem Nat.map_swap_divisorsAntidiagonal {n : ℕ} : Finset.map (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) (Nat.divisorsAntidiagonal n) = Nat.divisorsAntidiagonal n

@[simp]

theorem Nat.image_fst_divisorsAntidiagonal {n : ℕ} : Finset.image Prod.fst (Nat.divisorsAntidiagonal n) = Nat.divisors n

@[simp]

theorem Nat.image_snd_divisorsAntidiagonal {n : ℕ} : Finset.image Prod.snd (Nat.divisorsAntidiagonal n) = Nat.divisors n

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₁).1 = ((fun (d : ℕ) => (d, n / d)) p₂).1) } (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₁).2 = ((fun (d : ℕ) => (n / d, d)) p₂).2) } (Nat.divisors n) = Nat.divisorsAntidiagonal n

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

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

• Nat.Perfect n = ((Finset.sum (Nat.properDivisors n) fun (i : ℕ) => i) = n ∧ 0 < n)

theorem Nat.perfect_iff_sum_properDivisors {n : ℕ} (h : 0 < n) : Nat.Perfect n ↔ (Finset.sum (Nat.properDivisors n) fun (i : ℕ) => i) = n

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

theorem Nat.mem_divisors_prime_pow {p : ℕ} (pp : Nat.Prime p) (k : ℕ) {x : ℕ} : x ∈ Nat.divisors (p ^ k) ↔ ∃ j ≤ k, x = p ^ j

theorem Nat.Prime.divisors {p : ℕ} (pp : Nat.Prime p) : Nat.divisors p = {1, p}

theorem Nat.Prime.properDivisors {p : ℕ} (pp : Nat.Prime p) : Nat.properDivisors p = {1}

theorem Nat.divisors_prime_pow {p : ℕ} (pp : Nat.Prime p) (k : ℕ) : Nat.divisors (p ^ k) = Finset.map { toFun := fun (x : ℕ) => p ^ x, inj' := (_ : Function.Injective fun (x : ℕ) => p ^ x) } (Finset.range (k + 1))

theorem Nat.divisors_injective : Function.Injective Nat.divisors

@[simp]

theorem Nat.divisors_inj {a : ℕ} {b : ℕ} : Nat.divisors a = Nat.divisors b ↔ a = b

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

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} [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} [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} [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} [CommMonoid α] {p : ℕ} {f : ℕ → α} (h : Nat.Prime p) : (Finset.prod (Nat.divisors p) fun (x : ℕ) => f x) = f p * f 1

theorem Nat.properDivisors_eq_singleton_one_iff_prime {n : ℕ} : Nat.properDivisors n = {1} ↔ Nat.Prime n

theorem Nat.sum_properDivisors_eq_one_iff_prime {n : ℕ} : (Finset.sum (Nat.properDivisors n) fun (x : ℕ) => x) = 1 ↔ Nat.Prime n

theorem Nat.mem_properDivisors_prime_pow {p : ℕ} (pp : Nat.Prime p) (k : ℕ) {x : ℕ} : x ∈ Nat.properDivisors (p ^ k) ↔ ∃ (j : ℕ) (_ : j < k), x = p ^ j

theorem Nat.properDivisors_prime_pow {p : ℕ} (pp : Nat.Prime p) (k : ℕ) : Nat.properDivisors (p ^ k) = Finset.map { toFun := fun (x : ℕ) => p ^ x, inj' := (_ : Function.Injective fun (x : ℕ) => p ^ x) } (Finset.range k)

@[simp]

theorem Nat.sum_properDivisors_prime_nsmul {α : Type u_1} [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} [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} [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} [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} [AddCommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} : (Finset.sum (Nat.divisorsAntidiagonal n) fun (i : ℕ × ℕ) => f i.1 i.2) = Finset.sum (Nat.divisors n) fun (i : ℕ) => f i (n / i)

theorem Nat.prod_divisorsAntidiagonal {M : Type u_1} [CommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} : (Finset.prod (Nat.divisorsAntidiagonal n) fun (i : ℕ × ℕ) => f i.1 i.2) = Finset.prod (Nat.divisors n) fun (i : ℕ) => f i (n / i)

theorem Nat.sum_divisorsAntidiagonal' {M : Type u_1} [AddCommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} : (Finset.sum (Nat.divisorsAntidiagonal n) fun (i : ℕ × ℕ) => f i.1 i.2) = Finset.sum (Nat.divisors n) fun (i : ℕ) => f (n / i) i

theorem Nat.prod_divisorsAntidiagonal' {M : Type u_1} [CommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} : (Finset.prod (Nat.divisorsAntidiagonal n) fun (i : ℕ × ℕ) => f i.1 i.2) = Finset.prod (Nat.divisors n) fun (i : ℕ) => f (n / i) i

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

theorem Nat.prime_divisors_filter_dvd_of_dvd {m : ℕ} {n : ℕ} (hn : n ≠ 0) (hmn : m ∣ n) : Finset.filter (fun (x : ℕ) => x ∣ m) (List.toFinset (Nat.factors n)) = List.toFinset (Nat.factors m)

@[simp]

theorem Nat.image_div_divisors_eq_divisors (n : ℕ) : Finset.image (fun (x : ℕ) => n / x) (Nat.divisors n) = Nat.divisors n

theorem Nat.sum_div_divisors {α : Type u_1} [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} [CommMonoid α] (n : ℕ) (f : ℕ → α) : (Finset.prod (Nat.divisors n) fun (d : ℕ) => f (n / d)) = Finset.prod (Nat.divisors n) f