completedCosZeta₀_neg — Mathlib

English

Negation in the a-argument leaves completedCosZeta₀ unchanged: completedCosZeta₀(−a, s) = completedCosZeta₀(a, s).

Русский

Замена a на −a не изменяет completedCosZeta₀: completedCosZeta₀(−a, s) = completedCosZeta₀(a, s).

LaTeX

$$$$ \\operatorname{completedCosZeta}_0(-a,s) = \\operatorname{completedCosZeta}_0(a,s). $$$$

Lean4

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

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