mathlib3

6816b835 - feat(archive/100-theorems-list/70_perfect_numbers): Direction 1 of the Perfect Number Theorem (#4544)

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.