sigma_zero_mul_of_coprime
plain-language theorem explainer
The theorem establishes that the divisor-counting function σ_0 satisfies σ_0(mn) = σ_0(m) σ_0(n) for coprime natural numbers m and n. Number theorists working with arithmetic functions or preparing Dirichlet inversion steps would cite this multiplicativity. The proof is a direct one-line application of the general σ_k multiplicativity result.
Claim. Let $m, n$ be coprime natural numbers. Then $σ_0(mn) = σ_0(m) σ_0(n)$, where $σ_0$ denotes the sum-of-divisors function with exponent zero (the divisor function $d(n)$).
background
The ArithmeticFunctions module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Here sigma is the abbreviation sigma k := ArithmeticFunction.sigma k, so that σ_k(n) sums d^k over positive divisors d of n. For k = 0 this reduces to the number of divisors. The module keeps statements minimal to support later Dirichlet algebra once basic interfaces stabilize.
proof idea
This is a one-line wrapper that applies the upstream theorem sigma_mul_of_coprime (the general case σ_k(mn) = σ_k(m) σ_k(n) for any fixed k) directly to k = 0.
why it matters
It specializes the general multiplicativity of σ_k to the divisor-counting case σ_0, filling a basic arithmetic-function identity needed for prime-related manipulations in the module. No downstream uses are recorded yet. It supports the module's stated goal of providing Möbius footholds without yet touching the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.