sum_totient' — Mathlib

English

Equivalent statement: the sum over divisors d of n of φ(d) equals n.

Русский

Эквивалентное утверждение: сумма φ(d) по всем делителям d числа n равна n.

LaTeX

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

Lean4

theorem sum_totient' (n : ℕ) : ∑ m ∈ range n.succ with m ∣ n, φ m = n :=
  by
  convert sum_totient _ using 1
  simp only [Nat.divisors, sum_filter, range_eq_Ico]
  rw [sum_eq_sum_Ico_succ_bot] <;> simp

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