mathlib documentation

data.nat.totient

def nat.totient (n : ℕ) :

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

@[simp]

theorem nat.totient_zero :

theorem nat.totient_le (n : ℕ) :

n.totient ≤ n

theorem nat.totient_pos {n : ℕ} (a : 0 < n) :

theorem nat.sum_totient (n : ℕ) :

∑ (m : ℕ) in finset.filter (λ (_x : ℕ), _x ∣ n) (finset.range n.succ), m.totient = n