zeta_pos

Mathlib.NumberTheory.ArithmeticFunction

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

English

For every natural x, ζ(x) > 0 if and only if x > 0.

Русский

Для каждого натурального числа x выполняется: ζ(x) > 0 тогда и только тогда, когда x > 0.

LaTeX

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

Lean4

theorem zeta_pos {x : ℕ} : 0 < ζ x ↔ 0 < x := by simp [Nat.pos_iff_ne_zero]

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

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

Разделы

Аффилиация

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