odd_totient_iff — Mathlib

English

For every natural number n, φ(n) is odd if and only if n equals 1 or 2.

Русский

Для любого натурального числа n φ(n) нечётно тогда и только тогда, когда n = 1 или n = 2.

LaTeX

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

Lean4

/-- Euler's totient function is only odd at `1` or `2`. -/
theorem odd_totient_iff {n : ℕ} : Odd (φ n) ↔ n = 1 ∨ n = 2 := by
  rcases n with _ | _ | _ | _ <;> simp [Nat.totient_even]

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