totient_even — Mathlib

English

If m and n are coprime, then φ(mn) = φ(m) φ(n).

Русский

Если m и n взаимно просты, то φ(mn) = φ(m) φ(n).

LaTeX

$$$$\varphi(mn) = \varphi(m)\varphi(n) \quad\text{if } \gcd(m,n)=1.$$$$

Lean4

theorem totient_even {n : ℕ} (hn : 2 < n) : Even n.totient :=
  by
  haveI : Fact (1 < n) := ⟨one_lt_two.trans hn⟩
  haveI : NeZero n := NeZero.of_gt hn
  suffices 2 = orderOf (-1 : (ZMod n)ˣ)
    by
    rw [← ZMod.card_units_eq_totient, even_iff_two_dvd, this]
    exact orderOf_dvd_card
  rw [← orderOf_units, Units.coe_neg_one, orderOf_neg_one, ringChar.eq (ZMod n) n, if_neg hn.ne']

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