sigma_eq_sum_div

Mathlib.NumberTheory.ArithmeticFunction

URI: https://scilib.ai/kg/mathlib#ArithmeticFunction.sigma_eq_sum_div

English

σ_k(n) equals the sum over divisors d of n of (n/d)^k.

Русский

σ_k(n) равно сумме по делителям d: (n/d)^k.

LaTeX

$$$ \sigma_k(n) = \sum_{d \mid n} (n/d)^k $$$

Lean4

theorem sigma_eq_sum_div (k n : ℕ) : sigma k n = ∑ d ∈ Nat.divisors n, (n / d) ^ k := by
  rw [sigma_apply, ← Nat.sum_div_divisors]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru