perfect_iff_sum_divisors_eq_two_mul

English

For n > 0, Perfect(n) iff the sum of divisors equals 2n.

Русский

Для n > 0 соверешенное число эквивалентно тому, что сумма делителей равна 2n.

LaTeX

$$$ 0 < n \Rightarrow (\text{Perfect}(n) \iff \sum_{i \in \mathrm{divisors}(n)} i = 2n)$$$

Lean4

theorem perfect_iff_sum_divisors_eq_two_mul (h : 0 < n) : Perfect n ↔ ∑ i ∈ divisors n, i = 2 * n :=
  by
  rw [perfect_iff_sum_properDivisors h, sum_divisors_eq_sum_properDivisors_add_self, two_mul]
  constructor <;> intro h
  · rw [h]
  · apply add_right_cancel h

Похожие утверждения