odd_totient_iff_eq_one

Mathlib.Data.Nat.Totient

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

English

For all n, φ(n) is odd if and only if φ(n) = 1.

Русский

Для всех n φ(n) нечётно тогда и только тогда, когда φ(n) = 1.

LaTeX

$$$$ \\forall n \\\\in \\\\mathbb{N}, \\\\operatorname{Odd}(\\\\phi(n)) \\\\iff \\\\varphi(n) = 1 $$$$

Lean4

theorem odd_totient_iff_eq_one {n : ℕ} : Odd (φ n) ↔ φ n = 1 := by simp [Nat.odd_totient_iff, Nat.totient_eq_one_iff]

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

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

Разделы

Аффилиация

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