Practical numbers

A positive integer $n$ is called a practical number if every positive integer $m ≤ n$ can be represented as a sum of distinct divisors of $n$.

References:

• Wikipedia, Practical number
• OEIS A005153

Main definitions

• Nat.IsPractical: A natural number $n$ is practical if every positive integer $m ≤ n$ can be expressed as a sum of distinct divisors of $n$.

def Nat.IsPractical (n : ℕ) : Prop

A natural number $n$ is practical if every positive integer $m ≤ n$ can be represented as a sum of distinct divisors of $n$.

Equations

• n.IsPractical = ∀ m ≤ n, m ∈ subsetSums ↑n.divisors