sigma_one_thirty
plain-language theorem explainer
Sigma_1 of 30 equals 72. Number theorists verifying arithmetic function tables for small composites would cite this evaluation. The proof is a direct native computation of the divisor sum.
Claim. $σ_1(30) = 72$, where $σ_k(n)$ is the sum of the $k$-th powers of all positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to the sum-of-divisors function. The local sigma is introduced as an abbreviation sigma (k : ℕ) that delegates to ArithmeticFunction.sigma k. This theorem supplies a concrete check for the composite 30 amid other small verifications in the file.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic expression directly.
why it matters
This supplies a basic numerical anchor for the sum-of-divisors function inside the arithmetic functions module. It supports the NumberTheory.Primes setup but carries no downstream citations. The declaration aligns with the framework's pattern of small-integer checks that accompany the phi-ladder and constant derivations elsewhere.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.