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), then 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.

References #

https://en.wikipedia.org/wiki/Euclid%E2%80%93Euler_theorem

source

theorem theorems_100.odd_mersenne_succ (k : ℕ) :

¬2 ∣ mersenne (k + 1)

source

theorem theorems_100.nat.sigma_two_pow_eq_mersenne_succ (k : ℕ) :

⇑(nat.arithmetic_function.sigma 1) (2 ^ k) = mersenne (k + 1)

source

theorem theorems_100.nat.perfect_two_pow_mul_mersenne_of_prime (k : ℕ) (pr : nat.prime (mersenne (k + 1))) :

(2 ^ k * mersenne (k + 1)).perfect

Euclid's theorem that Mersenne primes induce perfect numbers

source

theorem theorems_100.nat.ne_zero_of_prime_mersenne (k : ℕ) (pr : nat.prime (mersenne (k + 1))) :

k ≠ 0

source

theorem theorems_100.nat.even_two_pow_mul_mersenne_of_prime (k : ℕ) (pr : nat.prime (mersenne (k + 1))) :

even (2 ^ k * mersenne (k + 1))

source

theorem theorems_100.nat.eq_two_pow_mul_odd {n : ℕ} (hpos : 0 < n) :

∃ (k m : ℕ), n = 2 ^ k * m ∧ ¬even m

source

theorem theorems_100.nat.eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : even n) (perf : n.perfect) :

∃ (k : ℕ), nat.prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1)

Perfect Number Theorem: Euler's theorem that even perfect numbers can be factored as a power of two times a Mersenne prime.

source

theorem theorems_100.nat.even_and_perfect_iff {n : ℕ} :

even n ∧ n.perfect ↔ ∃ (k : ℕ), nat.prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1)

The Euclid-Euler theorem characterizing even perfect numbers