Perfect Numbers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file proves Theorem 70 from the 100 Theorems List.
The theorem characterizes even perfect numbers.
Euclid proved that if
2 ^ (k + 1) - 1 is prime (these primes are known as Mersenne primes),
2 ^ k * 2 ^ (k + 1) - 1 is perfect.
Euler proved the converse, that if
n is even and perfect, then there exists
k such that
n = 2 ^ k * 2 ^ (k + 1) - 1 and
2 ^ (k + 1) - 1 is prime.
Euclid's theorem that Mersenne primes induce perfect numbers
Perfect Number Theorem: Euler's theorem that even perfect numbers can be factored as a
power of two times a Mersenne prime.
The Euclid-Euler theorem characterizing even perfect numbers