English
For p > 0, φ(p) = p-1 if and only if p is prime.
Русский
Для p>0 условие φ(p) = p-1 эквивалентно p является простым.
LaTeX
$$$$\varphi(p) = p-1 \iff p \text{ is prime}.$$$
Lean4
theorem totient_eq_iff_prime {p : ℕ} (hp : 0 < p) : p.totient = p - 1 ↔ p.Prime :=
by
refine ⟨fun h => ?_, totient_prime⟩
replace hp : 1 < p := by
apply lt_of_le_of_ne
· rwa [succ_le_iff]
· rintro rfl
rw [totient_one, tsub_self] at h
exact one_ne_zero h
rw [totient_eq_card_coprime, range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico hp.le, Finset.filter_insert,
if_neg (not_coprime_of_dvd_of_dvd hp (dvd_refl p) (dvd_zero p)), ← Nat.card_Ico 1 p] at h
refine p.prime_of_coprime hp fun n hn hnz => Finset.filter_card_eq h n <| Finset.mem_Ico.mpr ⟨?_, hn⟩
cutsat
