completedHurwitzZetaEven₀_neg — Mathlib

English

The weak FE pair at a = 0 is symmetric; the symmetry relation is verified by simp.

Русский

Слабая ФЕ-пара при a = 0 симметрична; симметрическое тождество следует из simp.

LaTeX

$$$$ (\\mathrm{hurwitzEvenFEPair}(0)).\\mathrm{symm} = \\mathrm{hurwitzEvenFEPair}(0). $$$$

Lean4

@[simp]
theorem completedHurwitzZetaEven₀_neg (a : UnitAddCircle) (s : ℂ) :
    completedHurwitzZetaEven₀ (-a) s = completedHurwitzZetaEven₀ a s := by simp [completedHurwitzZetaEven₀]

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