zeta_apply_ne

Mathlib.NumberTheory.ArithmeticFunction

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

English

If x ≠ 0, then ζ(x) = 1.

Русский

Если x ≠ 0, то ζ(x) = 1.

LaTeX

$$$x \\neq 0 \\implies \\zeta(x) = 1$$$

Lean4

theorem zeta_apply_ne {x : ℕ} (h : x ≠ 0) : ζ x = 1 :=
  if_neg h

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

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

Разделы

Аффилиация

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