sigma_mul_of_coprime
plain-language theorem explainer
Number theorists cite the multiplicative property of the sum-of-divisors function when the arguments are coprime. It supports derivations of product formulas over coprime factors in arithmetic function theory. The proof is a one-line wrapper that unfolds the local sigma abbreviation and applies Mathlib's isMultiplicative_sigma.map_mul_of_coprime.
Claim. For any natural number $k$ and coprime natural numbers $m,n$, the sum-of-divisors function satisfies $σ_k(mn)=σ_k(m)·σ_k(n)$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. Here sigma is the abbreviation for the sum-of-divisors function σ_k, which sums d^k over the divisors d of its argument. The local theoretical setting keeps statements minimal so that Dirichlet algebra and inversion can be added once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper. It simplifies using the local definition of sigma, then applies the map_mul_of_coprime lemma from ArithmeticFunction.isMultiplicative_sigma.
why it matters
This result is invoked directly by sigma_one_mul_of_coprime and sigma_zero_mul_of_coprime, which specialize to the cases k=1 and k=0 and feed the totient product formula helpers. It supplies a basic multiplicative step inside the arithmetic functions module that supports Möbius inversion and prime-related calculations. No direct connection to the T0-T8 forcing chain appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.