sigma_one_ten
plain-language theorem explainer
The sum-of-divisors function σ_1 applied to 10 equals 18. Number theorists working with arithmetic functions in formal developments would cite this concrete evaluation. The proof is a direct computational check via native_decide on the definition of sigma.
Claim. $σ_1(10) = 18$
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 relevant sigma is the abbreviation sigma (k : ℕ) := ArithmeticFunction.sigma k, which for k=1 sums the divisors of its argument. The local setting keeps statements minimal to stabilize basic interfaces before layering Dirichlet algebra or inversion results.
proof idea
One-line wrapper that applies native_decide to evaluate the arithmetic function directly on the concrete inputs.
why it matters
This verification anchors the sigma definition inside the NumberTheory.Primes.ArithmeticFunctions module, which supplies Möbius footholds for later inversion work. It supplies a concrete instance of σ_1 that can be referenced when building toward prime-related arithmetic identities. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.