perfect_iff_sum_properDivisors — Mathlib

English

For n > 0, Perfect(n) is equivalent to the sum of proper divisors equaling n.

Русский

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

LaTeX

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

Lean4

theorem perfect_iff_sum_properDivisors (h : 0 < n) : Perfect n ↔ ∑ i ∈ properDivisors n, i = n :=
  and_iff_left h

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