totient_eq_one_iff — Mathlib

English

For every n, φ(n) = 1 if and only if n = 1 or n = 2.

Русский

Для каждого n: φ(n) = 1 тогда и только тогда, когда n = 1 или n = 2.

LaTeX

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

Lean4

theorem totient_eq_one_iff : ∀ {n : ℕ}, n.totient = 1 ↔ n = 1 ∨ n = 2
  | 0 => by simp
  | 1 => by simp
  | 2 => by simp
  | n + 3 => by
    have : 3 ≤ n + 3 := le_add_self
    simp only [succ_succ_ne_one, false_or]
    exact ⟨fun h => not_even_one.elim <| h ▸ totient_even this, by rintro ⟨⟩⟩

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