completedRiemannZeta₀_one_sub — Mathlib

English

The functional equation in Λ₀ form holds: Λ₀(1 - s) = Λ₀(s).

Русский

Функциональное уравнение в форме Λ₀: Λ₀(1 − s) = Λ₀(s).

LaTeX

$$$\\mathrm{completedRiemannZeta}_0(1 - s) = \\mathrm{completedRiemannZeta}_0(s)$$$

Lean4

/-- Riemann zeta functional equation, formulated for `Λ₀`: for any complex `s` we have
`Λ₀(1 - s) = Λ₀ s`. -/
theorem completedRiemannZeta₀_one_sub (s : ℂ) : completedRiemannZeta₀ (1 - s) = completedRiemannZeta₀ s := by
  rw [← completedHurwitzZetaEven₀_zero, ← completedCosZeta₀_zero, completedHurwitzZetaEven₀_one_sub]

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