hurwitzZetaEven_neg_two_mul_nat_add_one

English

HurwitzZetaEven vanishes at s = -2(n+1) for any a and n.

Русский

Значение HurwitzZetaEven равно нулю в s = -2(n+1) для любого a и n.

LaTeX

$$$\\forall a:\\text{UnitAddCircle},\\forall n\\in\\mathbb{N},\\,\\,\\mathrm{hurwitzZetaEven}(a, -2\\,(n+1)) = 0.$$$

Lean4

/-- The trivial zeroes of the even Hurwitz zeta function. -/
theorem hurwitzZetaEven_neg_two_mul_nat_add_one (a : UnitAddCircle) (n : ℕ) : hurwitzZetaEven a (-2 * (n + 1)) = 0 :=
  by
  have : (-2 : ℂ) * (n + 1) ≠ 0 := mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (Nat.cast_add_one_ne_zero n)
  rw [hurwitzZetaEven, Function.update_of_ne this, Gammaℝ_eq_zero_iff.mpr ⟨n + 1, by simp⟩, div_zero]

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