Divisor finsets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.
proper_divisors n is the finset of natural numbers that divide n, other than n.
divisors_antidiagonal 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 proper_divisors n is n.

Implementation details #

divisors 0, proper_divisors 0, and divisors_antidiagonal 0 are defined to be ∅.

Tags #

divisors, perfect numbers

source

def nat.divisors (n : ℕ) :

finset ℕ

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))

source

def nat.proper_divisors (n : ℕ) :

finset ℕ

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)

source

def nat.divisors_antidiagonal (n : ℕ) :

finset (ℕ × ℕ)

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))

source

@[simp]

theorem nat.filter_dvd_eq_divisors {n : ℕ} (h : n ≠ 0) :

finset.filter (λ (_x : ℕ), _x ∣ n) (finset.range n.succ) = n.divisors

source

@[simp]

theorem nat.filter_dvd_eq_proper_divisors {n : ℕ} (h : n ≠ 0) :

finset.filter (λ (_x : ℕ), _x ∣ n) (finset.range n) = n.proper_divisors

source

theorem nat.proper_divisors.not_self_mem {n : ℕ} :

n ∉ n.proper_divisors

source

@[simp]

theorem nat.mem_proper_divisors {n m : ℕ} :

n ∈ m.proper_divisors ↔ n ∣ m ∧ n < m

source

theorem nat.insert_self_proper_divisors {n : ℕ} (h : n ≠ 0) :

has_insert.insert n n.proper_divisors = n.divisors

source

theorem nat.cons_self_proper_divisors {n : ℕ} (h : n ≠ 0) :

finset.cons n n.proper_divisors nat.proper_divisors.not_self_mem = n.divisors

source

@[simp]

theorem nat.mem_divisors {n m : ℕ} :

n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0

source

theorem nat.one_mem_divisors {n : ℕ} :

1 ∈ n.divisors ↔ n ≠ 0

source

theorem nat.mem_divisors_self (n : ℕ) (h : n ≠ 0) :

n ∈ n.divisors

source

theorem nat.dvd_of_mem_divisors {n m : ℕ} (h : n ∈ m.divisors) :

n ∣ m

source

@[simp]

theorem nat.mem_divisors_antidiagonal {n : ℕ} {x : ℕ × ℕ} :

x ∈ n.divisors_antidiagonal ↔ x.fst * x.snd = n ∧ n ≠ 0

source

theorem nat.divisor_le {n m : ℕ} :

n ∈ m.divisors → n ≤ m

source

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

m.divisors ⊆ n.divisors

source

theorem nat.divisors_subset_proper_divisors {n m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) (hdiff : m ≠ n) :

m.divisors ⊆ n.proper_divisors

source

@[simp]

theorem nat.divisors_zero :

0.divisors = ∅

source

@[simp]

theorem nat.proper_divisors_zero :

0.proper_divisors = ∅

source

theorem nat.proper_divisors_subset_divisors {n : ℕ} :

n.proper_divisors ⊆ n.divisors

source

@[simp]

theorem nat.divisors_one :

1.divisors = {1}

source

@[simp]

theorem nat.proper_divisors_one :

1.proper_divisors = ∅

source

theorem nat.pos_of_mem_divisors {n m : ℕ} (h : m ∈ n.divisors) :

0 < m

source

theorem nat.pos_of_mem_proper_divisors {n m : ℕ} (h : m ∈ n.proper_divisors) :

0 < m

source

theorem nat.one_mem_proper_divisors_iff_one_lt {n : ℕ} :

1 ∈ n.proper_divisors ↔ 1 < n

source

@[simp]

theorem nat.divisors_antidiagonal_zero :

0.divisors_antidiagonal = ∅

source

@[simp]

theorem nat.divisors_antidiagonal_one :

1.divisors_antidiagonal = {(1, 1)}

source

@[simp]

theorem nat.swap_mem_divisors_antidiagonal {n : ℕ} {x : ℕ × ℕ} :

x.swap ∈ n.divisors_antidiagonal ↔ x ∈ n.divisors_antidiagonal

source

theorem nat.fst_mem_divisors_of_mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} (h : x ∈ n.divisors_antidiagonal) :

x.fst ∈ n.divisors

source

theorem nat.snd_mem_divisors_of_mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} (h : x ∈ n.divisors_antidiagonal) :

x.snd ∈ n.divisors

source

@[simp]

theorem nat.map_swap_divisors_antidiagonal {n : ℕ} :

finset.map (equiv.prod_comm ℕ ℕ).to_embedding n.divisors_antidiagonal = n.divisors_antidiagonal

source

@[simp]

theorem nat.image_fst_divisors_antidiagonal {n : ℕ} :

finset.image prod.fst n.divisors_antidiagonal = n.divisors

source

@[simp]

theorem nat.image_snd_divisors_antidiagonal {n : ℕ} :

finset.image prod.snd n.divisors_antidiagonal = n.divisors

source

theorem nat.map_div_right_divisors {n : ℕ} :

finset.map {to_fun := λ (d : ℕ), (d, n / d), inj' := _} n.divisors = n.divisors_antidiagonal

source

theorem nat.map_div_left_divisors {n : ℕ} :

finset.map {to_fun := λ (d : ℕ), (n / d, d), inj' := _} n.divisors = n.divisors_antidiagonal

source

theorem nat.sum_divisors_eq_sum_proper_divisors_add_self {n : ℕ} :

n.divisors.sum (λ (i : ℕ), i) = n.proper_divisors.sum (λ (i : ℕ), i) + n

source

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

n.perfect = (n.proper_divisors.sum (λ (i : ℕ), i) = n ∧ 0 < n)

source

theorem nat.perfect_iff_sum_proper_divisors {n : ℕ} (h : 0 < n) :

n.perfect ↔ n.proper_divisors.sum (λ (i : ℕ), i) = n

source

theorem nat.perfect_iff_sum_divisors_eq_two_mul {n : ℕ} (h : 0 < n) :

n.perfect ↔ n.divisors.sum (λ (i : ℕ), i) = 2 * n

source

theorem nat.mem_divisors_prime_pow {p : ℕ} (pp : nat.prime p) (k : ℕ) {x : ℕ} :

x ∈ (p ^ k).divisors ↔ ∃ (j : ℕ) (H : j ≤ k), x = p ^ j

source

theorem nat.prime.divisors {p : ℕ} (pp : nat.prime p) :

p.divisors = {1, p}

source

theorem nat.prime.proper_divisors {p : ℕ} (pp : nat.prime p) :

p.proper_divisors = {1}

source

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))

source

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

source

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

source

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

source

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

source

@[simp]

theorem nat.prime.sum_divisors {α : Type u_1} [add_comm_monoid α] {p : ℕ} {f : ℕ → α} (h : nat.prime p) :

p.divisors.sum (λ (x : ℕ), f x) = f p + f 1

source

@[simp]

theorem nat.prime.prod_divisors {α : Type u_1} [comm_monoid α] {p : ℕ} {f : ℕ → α} (h : nat.prime p) :

p.divisors.prod (λ (x : ℕ), f x) = f p * f 1

source

theorem nat.proper_divisors_eq_singleton_one_iff_prime {n : ℕ} :

n.proper_divisors = {1} ↔ nat.prime n

source

theorem nat.sum_proper_divisors_eq_one_iff_prime {n : ℕ} :

n.proper_divisors.sum (λ (x : ℕ), x) = 1 ↔ nat.prime n

source

theorem nat.mem_proper_divisors_prime_pow {p : ℕ} (pp : nat.prime p) (k : ℕ) {x : ℕ} :

x ∈ (p ^ k).proper_divisors ↔ ∃ (j : ℕ) (H : j < k), x = p ^ j

source

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)

source

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

source

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

source

@[simp]

theorem nat.sum_divisors_prime_pow {α : Type u_1} [add_comm_monoid α] {k p : ℕ} {f : ℕ → α} (h : nat.prime p) :

(p ^ k).divisors.sum (λ (x : ℕ), f x) = (finset.range (k + 1)).sum (λ (x : ℕ), f (p ^ x))

source

@[simp]

theorem nat.prod_divisors_prime_pow {α : Type u_1} [comm_monoid α] {k p : ℕ} {f : ℕ → α} (h : nat.prime p) :

(p ^ k).divisors.prod (λ (x : ℕ), f x) = (finset.range (k + 1)).prod (λ (x : ℕ), f (p ^ x))

source

theorem nat.prod_divisors_antidiagonal {M : Type u_1} [comm_monoid M] (f : ℕ → ℕ → M) {n : ℕ} :

n.divisors_antidiagonal.prod (λ (i : ℕ × ℕ), f i.fst i.snd) = n.divisors.prod (λ (i : ℕ), f i (n / i))

source

theorem nat.sum_divisors_antidiagonal {M : Type u_1} [add_comm_monoid M] (f : ℕ → ℕ → M) {n : ℕ} :

n.divisors_antidiagonal.sum (λ (i : ℕ × ℕ), f i.fst i.snd) = n.divisors.sum (λ (i : ℕ), f i (n / i))

source

theorem nat.prod_divisors_antidiagonal' {M : Type u_1} [comm_monoid M] (f : ℕ → ℕ → M) {n : ℕ} :

n.divisors_antidiagonal.prod (λ (i : ℕ × ℕ), f i.fst i.snd) = n.divisors.prod (λ (i : ℕ), f (n / i) i)

source

theorem nat.sum_divisors_antidiagonal' {M : Type u_1} [add_comm_monoid M] (f : ℕ → ℕ → M) {n : ℕ} :

n.divisors_antidiagonal.sum (λ (i : ℕ × ℕ), f i.fst i.snd) = n.divisors.sum (λ (i : ℕ), f (n / i) i)

source

theorem nat.prime_divisors_eq_to_filter_divisors_prime (n : ℕ) :

n.factors.to_finset = finset.filter nat.prime n.divisors

The factors of n are the prime divisors

source

@[simp]

theorem nat.image_div_divisors_eq_divisors (n : ℕ) :

finset.image (λ (x : ℕ), n / x) n.divisors = n.divisors

source

@[simp]

theorem nat.sum_div_divisors {α : Type u_1} [add_comm_monoid α] (n : ℕ) (f : ℕ → α) :

n.divisors.sum (λ (d : ℕ), f (n / d)) = n.divisors.sum f

source

@[simp]

theorem nat.prod_div_divisors {α : Type u_1} [comm_monoid α] (n : ℕ) (f : ℕ → α) :

n.divisors.prod (λ (d : ℕ), f (n / d)) = n.divisors.prod f