zeta_eq_zero

Mathlib.NumberTheory.ArithmeticFunction

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

English

Let ζ be the divisor-counting function given by ζ(n) = ∑_{d|n} 1. Then ζ(n) = 0 if and only if n = 0.

Русский

Пусть ζ — функция числа делителей: ζ(n) = ∑_{d|n} 1. Тогда ζ(n) = 0 тогда и только тогда, когда n = 0.

LaTeX

$$$$ \forall x \in \mathbb{N}, \zeta(x) = 0 \iff x = 0 $$$$

Lean4

theorem zeta_eq_zero {x : ℕ} : ζ x = 0 ↔ x = 0 := by simp [zeta]

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

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

Разделы

Аффилиация

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