Commit 2020-10-12 18:08 6816b835

View on Github →

feat(archive/100-theorems-list/70_perfect_numbers): Direction 1 of the Perfect Number Theorem (#4544) Proves Euclid's half of the Euclid-Euler Theorem that if 2 ^ (k + 1) - 1 is prime, then 2 ^ k * (2 ^ (k + 1) - 1) is an (even) perfect number.

Estimated changes

Created archive/100-theorems-list/70_perfect_numbers.lean

added theorem nat.even_two_pow_mul_mersenne_of_prime

added theorem nat.ne_zero_of_prime_mersenne

added theorem nat.perfect_two_pow_mul_mersenne_of_prime

added theorem nat.sigma_two_pow_eq_mersenne_succ

added theorem odd_mersenne_succ

Modified src/number_theory/arithmetic_function.lean

added theorem nat.arithmetic_function.sigma_one_apply

Modified src/number_theory/divisors.lean

added theorem nat.divisors_prime

added theorem nat.divisors_prime_pow

added theorem nat.mem_divisors_prime_pow

modified def nat.perfect

modified theorem nat.perfect_iff_sum_divisors_eq_two_mul

modified theorem nat.perfect_iff_sum_proper_divisors

added theorem nat.prod_divisors_prime

added theorem nat.prod_divisors_prime_pow

added theorem nat.sum_divisors_prime

added theorem nat.sum_divisors_prime_pow

Modified src/number_theory/lucas_lehmer.lean

added theorem succ_mersenne