deficient_iff_not_abundant_and_not_perfect

English

Let n ≠ 0. Then n is deficient iff n is not abundant and not perfect.

Русский

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

LaTeX

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

Lean4

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

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