sinZeta_eq — Mathlib

English

SinZeta is the imaginary part of expZeta: sinZeta(a,s) = (expZeta(a,s) − expZeta(-a,s))/(2i).

Русский

SinZeta есть мнимая часть expZeta: sinZeta(a,s) = (expZeta(a,s) − expZeta(-a,s))/(2i).

LaTeX

$$$$\\sinZeta(a,s) = \\frac{\\expZeta(a,s) - \\expZeta(-a,s)}{2i}.$$$$

Lean4

theorem sinZeta_eq (a : UnitAddCircle) (s : ℂ) : sinZeta a s = (expZeta a s - expZeta (-a) s) / (2 * I) :=
  by
  rw [expZeta, expZeta, cosZeta_neg, sinZeta_neg]
  field_simp
  ring_nf

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