deficient_or_perfect_or_abundant — Mathlib

English

For any n ≠ 0, Deficient n ∨ Abundant n ∨ Perfect n.

Русский

Для любого n ≠ 0 выполняется либо дефицитность, либо избыточность, либо совершенность.

LaTeX

$$$n \neq 0 \rightarrow \operatorname{Deficient}(n) \lor \operatorname{Abundant}(n) \lor \operatorname{Perfect}(n)$$$

Lean4

/-- A positive natural number is either deficient, perfect, or abundant -/
theorem deficient_or_perfect_or_abundant (hn : 0 ≠ n) : Deficient n ∨ Abundant n ∨ Perfect n :=
  by
  dsimp only [Perfect, Abundant, Deficient]
  cutsat

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