sigma_isMultiplicative
plain-language theorem explainer
The sum-of-divisors function σ_k is multiplicative for every natural number k. Number theorists using Dirichlet convolution or Euler products cite this when reducing divisor sums to prime-power factors. The proof is a one-line wrapper that unfolds the local sigma abbreviation and invokes the corresponding Mathlib fact.
Claim. For every natural number $k$, the arithmetic function defined by $σ_k(n) = ∑_{d|n} d^k$ satisfies $σ_k(mn) = σ_k(m)σ_k(n)$ whenever $gcd(m,n)=1$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to the sum-of-divisors family. The local definition of sigma is the abbreviation sigma (k : ℕ) := ArithmeticFunction.sigma k, which directly imports the standard sum-of-divisors function. Upstream results include the AbileneParadox sigma (an unrelated agent-report gap) and the UniversalForcingSelfReference structure (a meta-realization certificate), but the relevant dependency for this theorem is the arithmetic sigma abbreviation itself.
proof idea
The term-mode proof first applies simp only [sigma] to replace the local abbreviation with the Mathlib ArithmeticFunction.sigma, then invokes the exact lemma ArithmeticFunction.isMultiplicative_sigma.
why it matters
This theorem supplies the multiplicativity property required for Euler-product expansions and Dirichlet-series manipulations inside the arithmetic-functions module. The module itself positions these wrappers as Möbius footholds for later inversion formulas. It sits in the NumberTheory.Primes layer that supports the Recognition Science forcing chain by furnishing standard multiplicative tools without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.