sinZeta_neg_two_mul_nat_sub_one — Mathlib

English

The sine zeta function vanishes at the odd negative integers: sinZeta(a, −(2n+1)) = 0 for all a and n ∈ ℕ.

Русский

У синус-зеты нули в нечетных отрицательных целых: sinZeta(a, −(2n+1)) = 0 для всех a и n∈ℕ.

LaTeX

$$$$ \sinZeta\left(a,-(2n+1)\right) = 0, \quad \forall a \in \mathrm{UnitAddCircle}, \; n\in\mathbb{N}. $$$$

Lean4

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

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