data.nat.totient

# Euler's totient function #

This file defines [Euler's totient function][https://en.wikipedia.org/wiki/Euler's_totient_function] nat.totient n which counts the number of naturals less than n that are coprime with n. We prove the divisor sum formula, namely that n equals φ summed over the divisors of n. See sum_totient.

def nat.totient (n : ) :

Euler's totient function. This counts the number of naturals strictly less than n which are coprime with n.

Equations
@[simp]
theorem nat.totient_zero  :
theorem nat.totient_le (n : ) :
theorem nat.totient_pos {n : } :
0 < n0 < n.totient
theorem nat.sum_totient (n : ) :
∑ (m : ) in finset.filter (λ (_x : ), _x n) (finset.range n.succ), m.totient = n