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.

Conventions

Since 0 has infinitely many divisors, none of the definitions in this file make sense for it. Therefore we adopt the convention that Nat.divisors 0, Nat.properDivisors 0, Nat.divisorsAntidiagonal 0 and Int.divisorsAntidiag 0 are all ∅.

Tags

divisors, perfect numbers

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

divisors n is the Finset of divisors of n. By convention, we set divisors 0 = ∅.

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

properDivisors n is the Finset of divisors of n, other than n. By convention, we set properDivisors 0 = ∅.

def Nat.divisorsAntidiagonal (n : ℕ) : Finset (ℕ × ℕ)

Pairs of divisors of a natural number as a finset.

n.divisorsAntidiagonal is the finset of pairs (a, b) : ℕ × ℕ such that a * b = n. By convention, we set Nat.divisorsAntidiagonal 0 = ∅.

O(n).

def Nat.divisorsAntidiagonalList (n : ℕ) : List (ℕ × ℕ)

Pairs of divisors of a natural number, as a list.

n.divisorsAntidiagonalList is the list of pairs (a, b) : ℕ × ℕ such that a * b = n, ordered by increasing a. By convention, we set Nat.divisorsAntidiagonalList 0 = [].

@[simp]

theorem Nat.filter_dvd_eq_divisors {n : ℕ} (h : n ≠ 0) : {d ∈ Finset.range n.succ | d ∣ n} = n.divisors

@[simp]

theorem Nat.filter_dvd_eq_properDivisors {n : ℕ} (h : n ≠ 0) : {d ∈ Finset.range n | d ∣ n} = n.properDivisors

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

@[simp]

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

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

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

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

theorem Nat.ne_zero_of_mem_divisors {n m : ℕ} (h : n ∈ m.divisors) : m ≠ 0

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

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

@[simp]

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

@[simp]

theorem Nat.divisorsAntidiagonalList_zero : divisorsAntidiagonalList 0 = []

@[simp]

theorem Nat.divisorsAntidiagonalList_one : divisorsAntidiagonalList 1 = [(1, 1)]

@[simp]

theorem Nat.toFinset_divisorsAntidiagonalList {n : ℕ} : n.divisorsAntidiagonalList.toFinset = n.divisorsAntidiagonal

theorem Nat.pairwise_divisorsAntidiagonalList_fst {n : ℕ} : List.Pairwise (fun (x1 x2 : ℕ × ℕ) => x1.1 < x2.1) n.divisorsAntidiagonalList

theorem Nat.pairwise_divisorsAntidiagonalList_snd {n : ℕ} : List.Pairwise (fun (x1 x2 : ℕ × ℕ) => x1.2 > x2.2) n.divisorsAntidiagonalList

@[deprecated Nat.pairwise_divisorsAntidiagonalList_fst (since := "2025-11-27")]

theorem Nat.sorted_divisorsAntidiagonalList_fst {n : ℕ} : List.Pairwise (fun (x1 x2 : ℕ × ℕ) => x1.1 < x2.1) n.divisorsAntidiagonalList

Alias of Nat.pairwise_divisorsAntidiagonalList_fst.

@[deprecated Nat.pairwise_divisorsAntidiagonalList_snd (since := "2025-11-27")]

theorem Nat.sorted_divisorsAntidiagonalList_snd {n : ℕ} : List.Pairwise (fun (x1 x2 : ℕ × ℕ) => x1.2 > x2.2) n.divisorsAntidiagonalList

Alias of Nat.pairwise_divisorsAntidiagonalList_snd.

theorem Nat.sortedLT_map_fst_divisorsAntidiagonalList {n : ℕ} : (List.map Prod.fst n.divisorsAntidiagonalList).SortedLT

theorem Nat.sortedGT_map_snd_divisorsAntidiagonalList {n : ℕ} : (List.map Prod.snd n.divisorsAntidiagonalList).SortedGT

theorem Nat.nodup_divisorsAntidiagonalList {n : ℕ} : n.divisorsAntidiagonalList.Nodup

@[simp]

theorem Nat.val_divisorsAntidiagonal (n : ℕ) : n.divisorsAntidiagonal.val = ↑n.divisorsAntidiagonalList

The Finset and List versions agree by definition.

@[simp]

theorem Nat.mem_divisorsAntidiagonalList {n : ℕ} {a : ℕ × ℕ} : a ∈ n.divisorsAntidiagonalList ↔ a.1 * a.2 = n ∧ n ≠ 0

@[simp]

theorem Nat.swap_mem_divisorsAntidiagonalList {n : ℕ} {a : ℕ × ℕ} : a.swap ∈ n.divisorsAntidiagonalList ↔ a ∈ n.divisorsAntidiagonalList

theorem Nat.reverse_divisorsAntidiagonalList (n : ℕ) : n.divisorsAntidiagonalList.reverse = List.map Prod.swap n.divisorsAntidiagonalList

theorem Nat.ne_zero_of_mem_divisorsAntidiagonal {n : ℕ} {p : ℕ × ℕ} (hp : p ∈ n.divisorsAntidiagonal) : p.1 ≠ 0 ∧ p.2 ≠ 0

theorem Nat.left_ne_zero_of_mem_divisorsAntidiagonal {n : ℕ} {p : ℕ × ℕ} (hp : p ∈ n.divisorsAntidiagonal) : p.1 ≠ 0

theorem Nat.right_ne_zero_of_mem_divisorsAntidiagonal {n : ℕ} {p : ℕ × ℕ} (hp : p ∈ n.divisorsAntidiagonal) : p.2 ≠ 0

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

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

theorem Nat.card_divisors_le_self (n : ℕ) : n.divisors.card ≤ n

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

theorem Nat.divisors_filter_dvd_of_dvd {n m : ℕ} (hn : n ≠ 0) (hm : m ∣ n) : {d ∈ n.divisors | d ∣ m} = m.divisors

@[simp]

theorem Nat.divisors_zero : divisors 0 = ∅

@[simp]

theorem Nat.properDivisors_zero : properDivisors 0 = ∅

@[simp]

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

@[simp]

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

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

@[simp]

theorem Nat.divisors_one : divisors 1 = {1}

@[simp]

theorem Nat.properDivisors_one : properDivisors 1 = ∅

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

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

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

@[simp]

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

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

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

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

See also Nat.mem_properDivisors.

@[simp]

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

@[simp]

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

@[simp]

theorem Nat.divisorsAntidiagonal_zero : divisorsAntidiagonal 0 = ∅

@[simp]

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

@[simp]

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

theorem Nat.prodMk_mem_divisorsAntidiag {n x y : ℕ} (hn : n ≠ 0) : (x, y) ∈ n.divisorsAntidiagonal ↔ x * y = n

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

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Nat.map_div_right_divisors {n : ℕ} : Finset.map { toFun := fun (d : ℕ) => (d, n / d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal

theorem Nat.map_div_left_divisors {n : ℕ} : Finset.map { toFun := fun (d : ℕ) => (n / d, d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal

theorem Nat.sum_divisors_eq_sum_properDivisors_add_self {n : ℕ} : ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, 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.

theorem Nat.perfect_iff_sum_properDivisors {n : ℕ} (h : 0 < n) : n.Perfect ↔ ∑ i ∈ n.properDivisors, i = n

theorem Nat.perfect_iff_sum_divisors_eq_two_mul {n : ℕ} (h : 0 < n) : n.Perfect ↔ ∑ i ∈ n.divisors, i = 2 * n

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

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

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

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

theorem Nat.divisors_injective : Function.Injective divisors

@[simp]

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

theorem Nat.eq_properDivisors_of_subset_of_sum_eq_sum {n : ℕ} {s : Finset ℕ} (hsub : s ⊆ n.properDivisors) : ∑ x ∈ s, x = ∑ x ∈ n.properDivisors, x → s = n.properDivisors

theorem Nat.sum_properDivisors_dvd {n : ℕ} (h : ∑ x ∈ n.properDivisors, x ∣ n) : ∑ x ∈ n.properDivisors, x = 1 ∨ ∑ x ∈ n.properDivisors, x = n

@[simp]

theorem Nat.Prime.prod_properDivisors {α : Type u_1} [CommMonoid α] {p : ℕ} {f : ℕ → α} (h : Prime p) : ∏ x ∈ p.properDivisors, f x = f 1

@[simp]

theorem Nat.Prime.sum_properDivisors {α : Type u_1} [AddCommMonoid α] {p : ℕ} {f : ℕ → α} (h : Prime p) : ∑ x ∈ p.properDivisors, f x = f 1

@[simp]

theorem Nat.Prime.prod_divisors {α : Type u_1} [CommMonoid α] {p : ℕ} {f : ℕ → α} (h : Prime p) : ∏ x ∈ p.divisors, f x = f p * f 1

@[simp]

theorem Nat.Prime.sum_divisors {α : Type u_1} [AddCommMonoid α] {p : ℕ} {f : ℕ → α} (h : Prime p) : ∑ x ∈ p.divisors, f x = f p + f 1

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

theorem Nat.sum_properDivisors_eq_one_iff_prime {n : ℕ} : ∑ x ∈ n.properDivisors, x = 1 ↔ Prime n

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

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

@[simp]

theorem Nat.prod_properDivisors_prime_pow {α : Type u_1} [CommMonoid α] {k p : ℕ} {f : ℕ → α} (h : Prime p) : ∏ x ∈ (p ^ k).properDivisors, f x = ∏ x ∈ Finset.range k, f (p ^ x)

@[simp]

theorem Nat.sum_properDivisors_prime_nsmul {α : Type u_1} [AddCommMonoid α] {k p : ℕ} {f : ℕ → α} (h : Prime p) : ∑ x ∈ (p ^ k).properDivisors, f x = ∑ x ∈ Finset.range k, f (p ^ x)

@[simp]

theorem Nat.prod_divisors_prime_pow {α : Type u_1} [CommMonoid α] {k p : ℕ} {f : ℕ → α} (h : Prime p) : ∏ x ∈ (p ^ k).divisors, f x = ∏ x ∈ Finset.range (k + 1), f (p ^ x)

@[simp]

theorem Nat.sum_divisors_prime_pow {α : Type u_1} [AddCommMonoid α] {k p : ℕ} {f : ℕ → α} (h : Prime p) : ∑ x ∈ (p ^ k).divisors, f x = ∑ x ∈ Finset.range (k + 1), f (p ^ x)

theorem Nat.prod_divisorsAntidiagonal {M : Type u_1} [CommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} : ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f i (n / i)

theorem Nat.sum_divisorsAntidiagonal {M : Type u_1} [AddCommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} : ∑ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∑ i ∈ n.divisors, f i (n / i)

theorem Nat.prod_divisorsAntidiagonal' {M : Type u_1} [CommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} : ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f (n / i) i

theorem Nat.sum_divisorsAntidiagonal' {M : Type u_1} [AddCommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} : ∑ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∑ i ∈ n.divisors, f (n / i) i

theorem Nat.primeFactors_eq_to_filter_divisors_prime (n : ℕ) : n.primeFactors = {p ∈ n.divisors | Prime p}

The factors of n are the prime divisors

theorem Nat.primeFactors_filter_dvd_of_dvd {m n : ℕ} (hn : n ≠ 0) (hmn : m ∣ n) : {p ∈ n.primeFactors | p ∣ m} = m.primeFactors

@[simp]

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

@[simp]

theorem Nat.prod_div_divisors {α : Type u_1} [CommMonoid α] (n : ℕ) (f : ℕ → α) : ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

@[simp]

theorem Nat.sum_div_divisors {α : Type u_1} [AddCommMonoid α] (n : ℕ) (f : ℕ → α) : ∑ d ∈ n.divisors, f (n / d) = n.divisors.sum f

theorem Nat.disjoint_divisors_filter_isPrimePow {a b : ℕ} (hab : a.Coprime b) : Disjoint (Finset.filter IsPrimePow a.divisors) (Finset.filter IsPrimePow b.divisors)

theorem Nat.divisorsAntidiagonal_eq_prod_filter_of_le {n N : ℕ} (n_ne_zero : n ≠ 0) (hn : n ≤ N) : n.divisorsAntidiagonal = {x ∈ Finset.Ioc 0 N ×ˢ Finset.Ioc 0 N | x.1 * x.2 = n}

Useful lemma for reordering sums.

def Int.divisorsAntidiag (z : ℤ) : Finset (ℤ × ℤ)

Pairs of divisors of an integer as a finset.

z.divisorsAntidiag is the finset of pairs (a, b) : ℤ × ℤ such that a * b = z. By convention, we set Int.divisorsAntidiag 0 = ∅.

O(|z|). Computed from Nat.divisorsAntidiagonal.

@[simp]

theorem Int.mem_divisorsAntidiag {z : ℤ} {xy : ℤ × ℤ} : xy ∈ z.divisorsAntidiag ↔ xy.1 * xy.2 = z ∧ z ≠ 0

@[simp]

theorem Int.divisorsAntidiag_zero : divisorsAntidiag 0 = ∅

@[simp]

theorem Int.divisorsAntidiagonal_one : divisorsAntidiag 1 = {(1, 1), (-1, -1)}

@[simp]

theorem Int.divisorsAntidiagonal_two : divisorsAntidiag 2 = {(1, 2), (2, 1), (-1, -2), (-2, -1)}

@[simp]

theorem Int.divisorsAntidiagonal_three : divisorsAntidiag 3 = {(1, 3), (3, 1), (-1, -3), (-3, -1)}

@[simp]

theorem Int.divisorsAntidiagonal_four : divisorsAntidiag 4 = {(1, 4), (2, 2), (4, 1), (-1, -4), (-2, -2), (-4, -1)}

theorem Int.prodMk_mem_divisorsAntidiag {x y z : ℤ} (hz : z ≠ 0) : (x, y) ∈ z.divisorsAntidiag ↔ x * y = z

@[simp]

theorem Int.swap_mem_divisorsAntidiag {xy : ℤ × ℤ} {z : ℤ} : xy.swap ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag

theorem Int.neg_mem_divisorsAntidiag {xy : ℤ × ℤ} {z : ℤ} : -xy ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag

@[simp]

theorem Int.map_prodComm_divisorsAntidiag {z : ℤ} : Finset.map (Equiv.prodComm ℤ ℤ).toEmbedding z.divisorsAntidiag = z.divisorsAntidiag

@[simp]

theorem Int.map_neg_divisorsAntidiag {z : ℤ} : Finset.map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag = z.divisorsAntidiag

theorem Int.divisorsAntidiag_neg {z : ℤ} : (-z).divisorsAntidiag = Finset.map ((Function.Embedding.refl ℤ).prodMap (Equiv.toEmbedding (Equiv.neg ℤ))) z.divisorsAntidiag

theorem Int.divisorsAntidiag_natCast (n : ℕ) : (↑n).divisorsAntidiag = (Finset.map (Nat.castEmbedding.prodMap Nat.castEmbedding) n.divisorsAntidiagonal).disjUnion (Finset.map ((Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))).prodMap (Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ)))) n.divisorsAntidiagonal) ⋯

theorem Int.divisorsAntidiag_neg_natCast (n : ℕ) : (-↑n).divisorsAntidiag = (Finset.map (Nat.castEmbedding.prodMap (Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ)))) n.divisorsAntidiagonal).disjUnion (Finset.map ((Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))).prodMap Nat.castEmbedding) n.divisorsAntidiagonal) ⋯

theorem Int.divisorsAntidiag_ofNat (n : ℕ) : (OfNat.ofNat n).divisorsAntidiag = (Finset.map (Nat.castEmbedding.prodMap Nat.castEmbedding) n.divisorsAntidiagonal).disjUnion (Finset.map ((Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))).prodMap (Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ)))) n.divisorsAntidiagonal) ⋯

theorem Int.mul_mem_one_two_three_iff {a b : ℤ} : a * b ∈ {1, 2, 3} ↔ (a, b) ∈ {(1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}

This lemma justifies its existence from its utility in crystallographic root system theory.

theorem Int.mul_mem_zero_one_two_three_four_iff {a b : ℤ} (h₀ : a = 0 ↔ b = 0) : a * b ∈ {0, 1, 2, 3, 4} ↔ (a, b) ∈ {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4), (-4, -1), (-1, -4), (2, 2), (-2, -2)}

This lemma justifies its existence from its utility in crystallographic root system theory.