sigma_one_mul_of_coprime
plain-language theorem explainer
The sum-of-divisors function at exponent 1 is multiplicative over coprime natural numbers. Analytic number theorists would cite this when decomposing divisor sums across coprime factors in prime factorization arguments. The proof is a one-line wrapper that specializes the general sigma_mul_of_coprime theorem to the case of exponent 1.
Claim. If $m$ and $n$ are coprime natural numbers, then $σ_1(mn) = σ_1(m) · σ_1(n)$, where $σ_1$ denotes the sum-of-divisors function.
background
The sum-of-divisors function $σ_k(n)$ sums the $k$-th powers of all divisors of $n$. In this module sigma k abbreviates ArithmeticFunction.sigma k from Mathlib, providing lightweight wrappers around arithmetic functions that begin with the Möbius function and prepare for Dirichlet algebra. The module setting keeps statements minimal until basic interfaces stabilize.
proof idea
This is a one-line wrapper that applies sigma_mul_of_coprime to the specific exponent 1, using the coprimality hypothesis directly.
why it matters
This supplies the multiplicativity of $σ_1$, a standard arithmetic identity required for handling divisor sums in the NumberTheory layer of the Recognition framework. It specializes the general sigma_mul_of_coprime result whose doc-comment states $σ_k(mn) = σ_k(m) × σ_k(n)$ for coprime $m,n$. No direct downstream uses are recorded yet, leaving it available for later identities supporting the phi-ladder or mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.