hurwitzZetaOdd_neg — Mathlib

English

The completed odd Hurwitz zeta is odd in a, i.e., completedHurwitzZetaOdd(-a) = - completedHurwitzZetaOdd(a).

Русский

Завершенная нечетная Хёрвитца ζ-функция нечетная по a: completedHurwitzZetaOdd(-a) = - completedHurwitzZetaOdd(a).

LaTeX

$$$$ completedHurwitzZetaOdd(-a) = - completedHurwitzZetaOdd(a). $$$$

Lean4

theorem hurwitzZetaOdd_neg (a : UnitAddCircle) (s : ℂ) : hurwitzZetaOdd (-a) s = -hurwitzZetaOdd a s := by
  simp_rw [hurwitzZetaOdd, completedHurwitzZetaOdd_neg, neg_div]

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