sum_totient — Mathlib

English

Equivalent formulation: the sum of totients over divisors equals n, as in sum_totient.

Русский

Эквивалентная формулировка: сумма φ по делителям равно n.

LaTeX

$$$$\sum_{d \mid n} φ(d) = n.$$$$

Lean4

theorem sum_totient (n : ℕ) : n.divisors.sum φ = n :=
  by
  rcases n.eq_zero_or_pos with (rfl | hn)
  · simp
  rw [← sum_div_divisors n φ]
  have : n = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d}) :=
    by
    nth_rw 1 [← card_range n]
    refine card_eq_sum_card_fiberwise fun x _ => mem_divisors.2 ⟨?_, hn.ne'⟩
    apply gcd_dvd_left
  nth_rw 3 [this]
  exact sum_congr rfl fun x hx => totient_div_of_dvd (dvd_of_mem_divisors hx)

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