totient_eq_card_coprime

Mathlib.Data.Nat.Totient

URI: https://scilib.ai/kg/mathlib#Nat.totient_eq_card_coprime

English

For any n, φ(n) equals the number of integers a with 0 ≤ a < n and gcd(a,n) = 1 (equivalently, a ∈ range(n) coprime to n).

Русский

Для любого n φ(n) равно числу целых a с 0 ≤ a < n и gcd(a,n) = 1 (то есть a ∈ range(n), coprime с n).

LaTeX

$$$$\varphi(n) = \#\{a ∈ \{0,1,\dots,n-1\} : \gcd(a,n)=1\}.$$$$

Lean4

theorem totient_eq_card_coprime (n : ℕ) : φ n = #({a ∈ range n | n.Coprime a}) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru