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 : ℕ is deficient if the sum of the proper divisors of n is less than n.

Equations

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
def Nat.Weird (n : ) :

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

Equations
theorem Nat.not_pseudoperfect_iff_forall {n : } :
¬n.Pseudoperfect n = 0 sn.properDivisors, is, i n

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

theorem Nat.Prime.not_weird {n : } (h : Prime n) :
theorem Nat.Prime.deficient_pow {n m : } (h : Prime n) :
(n ^ m).Deficient

Any natural number power of a prime is deficient

theorem Nat.Prime.deficient {n : } (h : Prime n) :

There exists infinitely many deficient numbers