The Dirichlet identity τ ∗ φ = σ

For every n, Σ_{d ∣ n} τ(d) φ(n/d) = σ(n), with τ the number of divisors, φ Euler's totient and σ the sum of divisors. In the ring of arithmetic functions τ = ζ ∗ ζ and φ ∗ ζ = id (Mathlib's Nat.sum_totient), so τ ∗ φ = ζ ∗ (ζ ∗ φ) = ζ ∗ id = σ.

Main results

• DivisorTotient.sum_card_divisors_mul_totient: sum over d | n of tau(d) * phi(n/d) equals sigma(n)

References

• Classical Dirichlet-series identity (e.g. G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, Ch. XVI). Found missing from Mathlib by excovery.identidades_mathlib.

theorem DivisorTotient.sum_card_divisors_mul_totient (n : ℕ) : ∑ d ∈ n.divisors, d.divisors.card * (n / d).totient = ∑ d ∈ n.divisors, d

Dirichlet identity τ ∗ φ = σ. For every n, Σ_{d ∣ n} τ(d) φ(n/d) = σ(n), where τ(d) is the number of divisors of d, φ Euler's totient and σ(n) the sum of the divisors of n.