odd_perfect_number.euler_form

A known result: If an odd perfect number exists, it must be of the form $p^α * m^2$ where $p$ is prime, $p \equiv 1 \pmod{4}$, $\alpha \equiv 1 \pmod{4}$, and $p \nmid m$. *Reference:* Euler's theorem on odd perfect numbers

theorem odd_perfect_number.euler_form (n : ℕ) (hn : Odd n) (hp : Perfect n) :
    ∃ (p m α : ℕ),
      p.Prime ∧
      p ≡ 1 [ZMOD 4] ∧
      α ≡ 1 [ZMOD 4] ∧
      ¬ p ∣ m ∧
      n = p^α * m^2

Recent Submissions

No submissions yet. Be the first to attempt this problem.