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 #
Nat.Abundant
: a natural numbern
is abundant if the sum of its proper divisors is greater thann
Nat.Pseudoperfect
: a natural numbern
is pseudoperfect if the sum of a subset of its proper divisors equalsn
Nat.Deficient
: a natural numbern
is deficient if the sum of its proper divisors is less thann
Nat.Weird
: a natural number is weird if it is abundant but not pseudoperfect
Main Results #
Nat.deficient_or_perfect_or_abundant
: A positive natural number is either deficient, perfect, or abundant.Nat.Prime.deficient
: All prime natural numbers are deficient.Nat.infinite_deficient
: There are infinitely many deficient numbers.Nat.Prime.deficient_pow
: Any natural number power of a prime is deficient.
Implementation Notes #
- Zero is not included in any of the definitions and these definitions only apply to natural numbers greater than zero.
References #
Tags #
abundant, deficient, weird, pseudoperfect
There exists infinitely many deficient numbers