totient_divisor_sum
plain-language theorem explainer
The identity that the sum of Euler's totient over the divisors of any natural number n recovers n is recorded as a thin wrapper. Number theorists and developers of arithmetic function libraries cite it when invoking the divisor-sum property of φ. The proof reduces directly to Mathlib's Nat.sum_totient after unfolding the local totient definition.
Claim. For every natural number $n$, $∑_{d|n} φ(d) = n$, where $φ$ denotes Euler's totient function.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to related maps such as totient. The local totient definition is the direct alias def totient (n : ℕ) : ℕ := Nat.totient n. The theorem sits inside the arithmetic-functions section whose module documentation describes the file as providing small wrappers around Mathlib's library, with deeper Dirichlet algebra to be layered later. The key upstream dependency is the totient wrapper itself together with Mathlib's Nat.sum_totient.
proof idea
The term-mode proof first applies simp only [totient] to replace the local wrapper by Nat.totient, then invokes the exact tactic on Nat.sum_totient n.
why it matters
The declaration supplies the classical divisor-sum identity for totient inside the arithmetic-functions module, completing a basic interface that the module documentation positions as a foothold for later Möbius inversion work. No downstream uses are recorded yet, so the result currently serves as a self-contained reference rather than a step toward a larger parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.