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) :
        Finset.filter (fun (x : ) => x n) (Finset.range n.succ) = n.divisors
        @[simp]
        theorem Nat.filter_dvd_eq_properDivisors {n : } (h : n 0) :
        Finset.filter (fun (x : ) => x n) (Finset.range n) = n.properDivisors
        theorem Nat.properDivisors.not_self_mem {n : } :
        nn.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.one_mem_divisors {n : } :
        1 n.divisors n 0
        theorem Nat.mem_divisors_self (n : ) (h : n 0) :
        n n.divisors
        theorem Nat.dvd_of_mem_divisors {n : } {m : } (h : n m.divisors) :
        n m
        @[simp]
        theorem Nat.mem_divisorsAntidiagonal {n : } {x : × } :
        x n.divisorsAntidiagonal x.1 * x.2 = n n 0
        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.divisorsn m
        theorem Nat.divisors_subset_of_dvd {n : } {m : } (hzero : n 0) (h : m n) :
        m.divisors n.divisors
        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) :
        Finset.filter (fun (x : ) => x m) n.divisors = m.divisors
        @[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.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
        theorem Nat.swap_mem_divisorsAntidiagonal {n : } {x : × } :
        x.swap n.divisorsAntidiagonal x n.divisorsAntidiagonal
        @[simp]
        theorem Nat.swap_mem_divisorsAntidiagonal_aux {n : } {x : × } :
        x.2 * x.1 = n ¬n = 0 x n.divisorsAntidiagonal
        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 : } :
        in.divisors, i = in.properDivisors, i + 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
        • n.Perfect = (in.properDivisors, i = n 0 < n)
        Instances For
          theorem Nat.perfect_iff_sum_properDivisors {n : } (h : 0 < n) :
          n.Perfect in.properDivisors, i = n
          theorem Nat.perfect_iff_sum_divisors_eq_two_mul {n : } (h : 0 < n) :
          n.Perfect in.divisors, i = 2 * n
          theorem Nat.mem_divisors_prime_pow {p : } (pp : Nat.Prime p) (k : ) {x : } :
          x (p ^ k).divisors jk, x = p ^ j
          theorem Nat.Prime.divisors {p : } (pp : Nat.Prime p) :
          p.divisors = {1, p}
          theorem Nat.Prime.properDivisors {p : } (pp : Nat.Prime p) :
          p.properDivisors = {1}
          theorem Nat.divisors_prime_pow {p : } (pp : Nat.Prime p) (k : ) :
          (p ^ k).divisors = Finset.map { toFun := fun (x : ) => p ^ x, inj' := } (Finset.range (k + 1))
          @[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) :
          xs, x = xn.properDivisors, xs = n.properDivisors
          theorem Nat.sum_properDivisors_dvd {n : } (h : xn.properDivisors, x n) :
          xn.properDivisors, x = 1 xn.properDivisors, x = n
          @[simp]
          theorem Nat.Prime.sum_properDivisors {α : Type u_1} [AddCommMonoid α] {p : } {f : α} (h : Nat.Prime p) :
          xp.properDivisors, f x = f 1
          @[simp]
          theorem Nat.Prime.prod_properDivisors {α : Type u_1} [CommMonoid α] {p : } {f : α} (h : Nat.Prime p) :
          xp.properDivisors, f x = f 1
          @[simp]
          theorem Nat.Prime.sum_divisors {α : Type u_1} [AddCommMonoid α] {p : } {f : α} (h : Nat.Prime p) :
          xp.divisors, f x = f p + f 1
          @[simp]
          theorem Nat.Prime.prod_divisors {α : Type u_1} [CommMonoid α] {p : } {f : α} (h : Nat.Prime p) :
          xp.divisors, f x = f p * f 1
          theorem Nat.sum_properDivisors_eq_one_iff_prime {n : } :
          xn.properDivisors, x = 1 Nat.Prime n
          theorem Nat.mem_properDivisors_prime_pow {p : } (pp : Nat.Prime p) (k : ) {x : } :
          x (p ^ k).properDivisors ∃ (j : ) (_ : j < k), x = p ^ j
          theorem Nat.properDivisors_prime_pow {p : } (pp : Nat.Prime p) (k : ) :
          (p ^ k).properDivisors = Finset.map { toFun := fun (x : ) => p ^ x, inj' := } (Finset.range k)
          @[simp]
          theorem Nat.sum_properDivisors_prime_nsmul {α : Type u_1} [AddCommMonoid α] {k : } {p : } {f : α} (h : Nat.Prime p) :
          x(p ^ k).properDivisors, f x = xFinset.range k, f (p ^ x)
          @[simp]
          theorem Nat.prod_properDivisors_prime_pow {α : Type u_1} [CommMonoid α] {k : } {p : } {f : α} (h : Nat.Prime p) :
          x(p ^ k).properDivisors, f x = xFinset.range k, f (p ^ x)
          @[simp]
          theorem Nat.sum_divisors_prime_pow {α : Type u_1} [AddCommMonoid α] {k : } {p : } {f : α} (h : Nat.Prime p) :
          x(p ^ k).divisors, f x = xFinset.range (k + 1), f (p ^ x)
          @[simp]
          theorem Nat.prod_divisors_prime_pow {α : Type u_1} [CommMonoid α] {k : } {p : } {f : α} (h : Nat.Prime p) :
          x(p ^ k).divisors, f x = xFinset.range (k + 1), f (p ^ x)
          theorem Nat.sum_divisorsAntidiagonal {M : Type u_1} [AddCommMonoid M] (f : M) {n : } :
          in.divisorsAntidiagonal, f i.1 i.2 = in.divisors, f i (n / i)
          theorem Nat.prod_divisorsAntidiagonal {M : Type u_1} [CommMonoid M] (f : M) {n : } :
          in.divisorsAntidiagonal, f i.1 i.2 = in.divisors, f i (n / i)
          theorem Nat.sum_divisorsAntidiagonal' {M : Type u_1} [AddCommMonoid M] (f : M) {n : } :
          in.divisorsAntidiagonal, f i.1 i.2 = in.divisors, f (n / i) i
          theorem Nat.prod_divisorsAntidiagonal' {M : Type u_1} [CommMonoid M] (f : M) {n : } :
          in.divisorsAntidiagonal, f i.1 i.2 = in.divisors, f (n / i) i

          The factors of n are the prime divisors

          @[deprecated Nat.primeFactors_eq_to_filter_divisors_prime]

          Alias of Nat.primeFactors_eq_to_filter_divisors_prime.


          The factors of n are the prime divisors

          theorem Nat.primeFactors_filter_dvd_of_dvd {m : } {n : } (hn : n 0) (hmn : m n) :
          Finset.filter (fun (x : ) => x m) n.primeFactors = m.primeFactors
          @[deprecated Nat.primeFactors_filter_dvd_of_dvd]
          theorem Nat.prime_divisors_filter_dvd_of_dvd {m : } {n : } (hn : n 0) (hmn : m n) :
          Finset.filter (fun (x : ) => x m) n.primeFactors = m.primeFactors

          Alias of Nat.primeFactors_filter_dvd_of_dvd.

          @[simp]
          theorem Nat.image_div_divisors_eq_divisors (n : ) :
          Finset.image (fun (x : ) => n / x) n.divisors = n.divisors
          theorem Nat.sum_div_divisors {α : Type u_1} [AddCommMonoid α] (n : ) (f : α) :
          dn.divisors, f (n / d) = n.divisors.sum f
          theorem Nat.prod_div_divisors {α : Type u_1} [CommMonoid α] (n : ) (f : α) :
          dn.divisors, f (n / d) = n.divisors.prod f