totient — Mathlib

English

Let n be a natural number. The totient φ(n) counts how many integers a with 1 ≤ a < n are coprime to n, i.e., gcd(a,n) = 1.

Русский

Пусть n — натуральное число. Функция Эйлера φ(n) считается количеством целых чисел a, таких что 1 ≤ a < n и gcd(a,n) = 1.

LaTeX

$$$$\varphi(n) = \#\{a \in \{1,2,\dots,n-1\} \mid \gcd(a,n)=1\}.$$$$

Lean4

/-- Euler's totient function. This counts the number of naturals strictly less than `n` which are
coprime with `n`. -/
def totient (n : ℕ) : ℕ :=
  #({a ∈ range n | n.Coprime a})

Похожие утверждения