practical_twentyeight
plain-language theorem explainer
The sum of the divisors of 28 equals 56 and therefore satisfies the inequality marking 28 as practical. Number theorists verifying practical numbers via divisor sums would cite this check. The proof uses a native decision procedure to confirm the concrete numerical fact.
Claim. Let $σ_1(28)$ denote the sum of the positive divisors of 28. Then $σ_1(28) ≥ 28$.
background
The module on arithmetic functions supplies small wrappers around Mathlib's library, beginning with the Möbius function. The sum-of-divisors function $σ_k(n)$ is defined as the sum of the k-th powers of the divisors of n. For the case k=1 and n=28 this yields the ordinary sum of divisors. The local theoretical setting keeps statements lightweight pending deeper Dirichlet algebra. An upstream definition maps this directly to the corresponding Mathlib construction.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the numerical inequality by direct computation.
why it matters
This declaration verifies the divisor-sum condition for the integer 28 to qualify as practical. It contributes to the arithmetic functions layer that supports prime computations in the framework. The module emphasizes basic interfaces without immediate downstream applications recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.