Odd Perfect Number

import Mathlib

-- Does there exist an odd perfect number?
-- (A number n is perfect if it equals the sum of its proper divisors.)
theorem no_odd_perfect : ∀ n : ℕ, Odd n → ¬(∑ d ∈ Nat.divisors n \ {n}, d = n) :=