completedRiemannZeta_one_sub — Mathlib

English

Another articulation of Λ's symmetry: Λ(1 - s) = Λ(s).

Русский

Ещё одно выражение симметрии Λ: Λ(1 − s) = Λ(s).

LaTeX

$$$\\mathrm{completedRiemannZeta}(1-s) = \\mathrm{completedRiemannZeta}(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]

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