sigma_zero_apply

Mathlib.NumberTheory.ArithmeticFunction

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

English

σ_0(n) equals the number of divisors of n.

Русский

σ_0(n) равно числу делителей n.

LaTeX

$$$ \sigma_0(n) = |\mathrm{divisors}(n)| $$$

Lean4

theorem sigma_zero_apply (n : ℕ) : σ 0 n = #n.divisors := by simp [sigma_apply]

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

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

Разделы

Аффилиация

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