sigma_zero_apply_prime_pow

Mathlib.NumberTheory.ArithmeticFunction

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

English

For prime p and i, σ_0(p^i) = i+1.

Русский

Для простого p и степени i: σ_0(p^i) = i+1.

LaTeX

$$$ \sigma_0(p^i) = i+1 $$$

Lean4

theorem sigma_zero_apply_prime_pow {p i : ℕ} (hp : p.Prime) : σ 0 (p ^ i) = i + 1 := by simp [sigma_apply_prime_pow hp]

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

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

Разделы

Аффилиация

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