sinZeta_neg — Mathlib

English

For every a in the unit circle and every complex s, sinZeta(−a, s) = − sinZeta(a, s); i.e., sinZeta is odd in the first argument.

Русский

Для всякого a из единичного круга и каждого комплексного s выполняется sinZeta(−a, s) = − sinZeta(a, s); синус-зета по первому аргументу нечетна.

LaTeX

$$$$ \sinZeta(-a,s) = -\sinZeta(a,s) $$$$

Lean4

theorem sinZeta_neg (a : UnitAddCircle) (s : ℂ) : sinZeta (-a) s = -sinZeta a s := by
  simp_rw [sinZeta, completedSinZeta_neg, neg_div]

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