completedCosZeta₀_zero — Mathlib

English

The zero-offset completed cosine zeta at 0 equals the zero-offset completed Riemann zeta.

Русский

Нулевой offset завершённой косинус-зеты эквивалентен Λ₀.

LaTeX

$$$\\mathrm{completedCosZeta}_0(0,s) = \\mathrm{completedRiemannZeta}_0(s)$$$

Lean4

theorem completedCosZeta₀_zero (s : ℂ) : completedCosZeta₀ 0 s = completedRiemannZeta₀ s := by
  rw [completedRiemannZeta₀, completedHurwitzZetaEven₀, completedCosZeta₀, hurwitzEvenFEPair_zero_symm]

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