sigma_one_apply_prime_pow

Mathlib.NumberTheory.ArithmeticFunction

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

English

For prime p and i, σ_1(p^i) = ∑_{k=0}^{i} p^{k}.

Русский

Для простого p и степени i: σ_1(p^i) = ∑_{k=0}^{i} p^{k}.

LaTeX

$$$ \sigma_1(p^i) = \sum_{k=0}^{i} p^{k} $$$

Lean4

theorem sigma_one_apply_prime_pow {p i : ℕ} (hp : p.Prime) : σ 1 (p ^ i) = ∑ k ∈ .range (i + 1), p ^ k := by
  simp [sigma_apply_prime_pow hp]

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

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

Разделы

Аффилиация

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