English
For all m,n ∈ ℕ, (φ(m)) and (φ(n)) are coprime if and only if one of m or n is 1 or 2.
Русский
Для любых m,n ∈ ℕ, φ(m) и φ(n) взаимно просты тогда и только тогда, когда хотя бы одно из m,n равно 1 или 2.
LaTeX
$$$$ (\\\\phi m) \\\\perp (\\\\phi n) \\\\iff ((m = 1 \\\\lor m = 2) \\\\lor (n = 1 \\\\lor n = 2)) $$$$
Lean4
/-- `Nat.totient m` and `Nat.totient n` are coprime iff one of them is 1. -/
theorem totient_coprime_totient_iff (m n : ℕ) : (φ m).Coprime (φ n) ↔ (m = 1 ∨ m = 2) ∨ (n = 1 ∨ n = 2) :=
by
constructor
· rw [← not_imp_not]
simp_rw [← odd_totient_iff, not_or, not_odd_iff_even, even_iff_two_dvd]
exact fun h ↦ Nat.not_coprime_of_dvd_of_dvd one_lt_two h.1 h.2
· simp_rw [← totient_eq_one_iff]
rintro (h | h) <;> rw [h]
exacts [Nat.coprime_one_left _, Nat.coprime_one_right _]
