Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-15 20:34 8985e395

View on Github →

feat(archive/100-theorems-list/70_perfect_numbers): Perfect Number Theorem, Direction 2 (#4621) Adds a few extra lemmas about divisors, proper_divisors and sums of proper divisors Proves Euler's direction of the Perfect Number theorem, finishing Freek 70

Estimated changes

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

added theorem nat.eq_pow_two_mul_odd

added theorem nat.eq_two_pow_mul_prime_mersenne_of_even_perfect

added theorem nat.even_and_perfect_iff

Modified docs/100.yaml

Modified src/number_theory/divisors.lean

added theorem nat.divisors_one

deleted theorem nat.divisors_prime

added theorem nat.eq_proper_divisors_of_subset_of_sum_eq_sum

modified theorem nat.fst_mem_divisors_of_mem_antidiagonal

modified theorem nat.map_swap_divisors_antidiagonal

added theorem nat.one_mem_proper_divisors_iff_one_lt

modified theorem nat.perfect_iff_sum_divisors_eq_two_mul

modified theorem nat.perfect_iff_sum_proper_divisors

added theorem nat.pos_of_mem_divisors

added theorem nat.pos_of_mem_proper_divisors

added theorem nat.prime.divisors

added theorem nat.prime.proper_divisors

added theorem nat.prime.sum_divisors

added theorem nat.prime.sum_proper_divisors

added theorem nat.proper_divisors_eq_singleton_one_iff_prime

added theorem nat.proper_divisors_one

added theorem nat.proper_divisors_subset_divisors

modified theorem nat.snd_mem_divisors_of_mem_antidiagonal

deleted theorem nat.sum_divisors_prime

added theorem nat.sum_proper_divisors_dvd

added theorem nat.sum_proper_divisors_eq_one_iff_prime

modified theorem nat.swap_mem_divisors_antidiagonal