Euler's totient function. This counts the number of positive integers less than n which are
coprime with n.
Equations
- n.totient = (finset.filter n.coprime (finset.range n)).card
theorem
nat.sum_totient
(n : ℕ) :
(finset.filter (λ (_x : ℕ), _x ∣ n) (finset.range n.succ)).sum (λ (m : ℕ), m.totient) = n