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
Instances For

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

    Equations
    Instances For

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

      Equations
      Instances For
        @[simp]
        theorem Nat.filter_dvd_eq_divisors {n : } (h : n 0) :
        @[simp]
        @[simp]
        theorem Nat.mem_properDivisors {n : } {m : } :
        @[simp]
        theorem Nat.mem_divisors {n : } {m : } :
        theorem Nat.mem_divisors_self (n : ) (h : n 0) :
        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.divisors_filter_dvd_of_dvd {n : } {m : } (hn : n 0) (hm : m n) :
        @[simp]
        theorem Nat.pos_of_mem_divisors {n : } {m : } (h : m Nat.divisors n) :
        0 < m
        @[simp]
        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
        Instances For
          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} [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.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} [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.fst i.snd) = 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.fst i.snd) = 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.fst i.snd) = 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.fst i.snd) = Finset.prod (Nat.divisors n) fun i => f (n / i) i
          theorem Nat.prime_divisors_filter_dvd_of_dvd {m : } {n : } (hn : n 0) (hmn : m 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