sigma_one
plain-language theorem explainer
The sum-of-divisors function evaluates to one at the argument one for any exponent k. Number theorists handling divisor sums or preparing Möbius inversion would cite this base case. The proof reduces directly to the explicit divisor-sum definition via a single simplification step.
Claim. For every natural number $k$, the sum-of-divisors function satisfies $σ_k(1)=1$.
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 sum-of-divisors function is introduced as the abbreviation sigma k standing for ArithmeticFunction.sigma k. Its action is recorded by the companion result that sigma k n equals the sum of d^k over all positive divisors d of n.
proof idea
The proof is a one-line wrapper that applies the sigma_apply theorem to replace the left-hand side by the explicit divisor sum at n=1, which collapses to the single term 1^ k.
why it matters
This evaluation supplies the base case needed for inductive arguments or generating-function identities involving the sum-of-divisors function inside the arithmetic-functions module. It sits upstream of any later Möbius-inversion statements that the module is positioned to host. No downstream citations are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.