Documentation

Mathlib.NumberTheory.FactorisationProperties

Factorisation properties of natural numbers #

This file defines abundant, pseudoperfect, deficient, and weird numbers and formalizes their relations with prime and perfect numbers.

Main Definitions #

Main Results #

Implementation Notes #

References #

Tags #

abundant, deficient, weird, pseudoperfect

def Nat.Abundant (n : ) :

n : ℕ is abundant if the sum of the proper divisors of n is greater than n.

Equations
  • n.Abundant = (n < in.properDivisors, i)
Instances For

    n : ℕ is deficient if the sum of the proper divisors of n is less than n.

    Equations
    • n.Deficient = (in.properDivisors, i < n)
    Instances For

      A positive natural number n is pseudoperfect if there exists a subset of the proper divisors of n such that the sum of that subset is equal to n.

      Equations
      • n.Pseudoperfect = (0 < n sn.properDivisors, is, i = n)
      Instances For
        def Nat.Weird (n : ) :

        n : ℕ is a weird number if and only if it is abundant but not pseudoperfect.

        Equations
        • n.Weird = (n.Abundant ¬n.Pseudoperfect)
        Instances For
          theorem Nat.not_pseudoperfect_iff_forall {n : } :
          ¬n.Pseudoperfect n = 0 sn.properDivisors, is, i n
          theorem Nat.deficient_iff_not_abundant_and_not_perfect {n : } (hn : n 0) :
          n.Deficient ¬n.Abundant ¬n.Perfect
          theorem Nat.perfect_iff_not_abundant_and_not_deficient {n : } (hn : 0 n) :
          n.Perfect ¬n.Abundant ¬n.Deficient
          theorem Nat.abundant_iff_not_perfect_and_not_deficient {n : } (hn : 0 n) :
          n.Abundant ¬n.Perfect ¬n.Deficient
          theorem Nat.deficient_or_perfect_or_abundant {n : } (hn : 0 n) :
          n.Deficient n.Abundant n.Perfect

          A positive natural number is either deficient, perfect, or abundant

          theorem Nat.Perfect.pseudoperfect {n : } (h : n.Perfect) :
          n.Pseudoperfect
          theorem Nat.Prime.not_abundant {n : } (h : Nat.Prime n) :
          ¬n.Abundant
          theorem Nat.Prime.not_weird {n : } (h : Nat.Prime n) :
          ¬n.Weird
          theorem Nat.Prime.not_pseudoperfect {p : } (h : Nat.Prime p) :
          ¬p.Pseudoperfect
          theorem Nat.Prime.not_perfect {p : } (h : Nat.Prime p) :
          ¬p.Perfect
          theorem Nat.Prime.deficient_pow {n : } {m : } (h : Nat.Prime n) :
          (n ^ m).Deficient

          Any natural number power of a prime is deficient

          theorem IsPrimePow.deficient {n : } (h : IsPrimePow n) :
          n.Deficient
          theorem Nat.Prime.deficient {n : } (h : Nat.Prime n) :
          n.Deficient
          theorem Nat.infinite_deficient :
          {n : | n.Deficient}.Infinite

          There exists infinitely many deficient numbers

          theorem Nat.infinite_even_deficient :
          {n : | Even n n.Deficient}.Infinite
          theorem Nat.infinite_odd_deficient :
          {n : | Odd n n.Deficient}.Infinite