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.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) :
        Finset.filter (fun (x : ) => x m) (Nat.divisors n) = Nat.divisors m
        @[simp]
        theorem Nat.nonempty_divisors {n : } :
        (Nat.divisors n).Nonempty n 0
        @[simp]
        @[simp]
        theorem Nat.pos_of_mem_divisors {n : } {m : } (h : m Nat.divisors n) :
        0 < m
        @[simp]
        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
        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
        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.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.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))
          @[simp]
          theorem Nat.divisors_inj {a : } {b : } :
          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 : ) (_ : 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_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