sigma_def
plain-language theorem explainer
The theorem supplies a simplification rule identifying the module-local sum-of-divisors function sigma k with Mathlib's standard ArithmeticFunction.sigma k. Number theorists extending prime-arithmetic results in Lean would cite it to inherit library lemmas without name clashes. The proof is a one-line reflexivity that holds because sigma is introduced as an abbreviation aliasing the library definition.
Claim. For each natural number $k$, the arithmetic function denoted sigma $k$ coincides exactly with the standard sum-of-divisors function sigma $k$ from the arithmetic-functions library.
background
The module supplies lightweight wrappers around Mathlib's arithmetic-function library, beginning with the Möbius function and extending to the sum-of-divisors function. The local sigma is introduced by the sibling abbreviation sigma (k : ℕ) : ArithmeticFunction ℕ := ArithmeticFunction.sigma k, so that sigma k stands for the function n ↦ ∑_{d∣n} d^k. The upstream AbileneParadox.sigma definition (a real-valued charge measuring private-public preference mismatch) is unrelated and appears only as a name collision in the import graph.
proof idea
The proof is a one-line wrapper that applies reflexivity. Because the left-hand side is literally defined to be the right-hand side, rfl closes the goal immediately.
why it matters
The declaration installs a simp lemma that lets downstream proofs invoke standard properties of the sum-of-divisors function without qualification. It occupies the arithmetic-functions layer that supports later prime-counting and divisor-sum arguments inside the NumberTheory.Primes hierarchy. No used-by edges are recorded yet, leaving open whether it will be invoked in explicit mass-ladder or phi-ladder calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.