hurwitzZetaOdd_neg_two_mul_nat_sub_one

English

Reformulation of the sine zeta Dirichlet-series representation via L-series; the same equality as above holds in the L-series framework.

Русский

Переформулировка представления синус-зета через L-ряд; то же равенство справедливо и в рамках L-рядов.

LaTeX

$$$$ \text{LSeriesHasSum}(\sin(2\pi a \cdot), s) = \sinZeta(a,s). $$$$

Lean4

/-- The trivial zeroes of the odd Hurwitz zeta function. -/
theorem hurwitzZetaOdd_neg_two_mul_nat_sub_one (a : UnitAddCircle) (n : ℕ) : hurwitzZetaOdd a (-2 * n - 1) = 0 := by
  rw [hurwitzZetaOdd, Gammaℝ_eq_zero_iff.mpr ⟨n, by rw [neg_mul, sub_add_cancel]⟩, div_zero]

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