perfect_iff_not_abundant_and_not_deficient

English

For any nonzero n, n is perfect iff not abundant and not deficient.

Русский

Пусть n ≠ 0. Тогда n совершенное тогда и только тогда, когда n не является ни избыточным, ни дефицитным.

LaTeX

$$$n \neq 0 \Rightarrow \operatorname{Perfect}(n) \iff (\lnot \operatorname{Abundant}(n) \land \lnot \operatorname{Deficient}(n))$$$

Lean4

theorem perfect_iff_not_abundant_and_not_deficient (hn : 0 ≠ n) : Perfect n ↔ ¬Abundant n ∧ ¬Deficient n :=
  by
  dsimp only [Perfect, Abundant, Deficient]
  cutsat

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