mathlib documentation

data.nat.totient

def nat.totient  :

Euler's totient function. This counts the number of positive integers 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