cosZeta_eq — Mathlib

English

CosZeta is the average of expZeta(a,s) and expZeta(-a,s): cosZeta(a,s) = (expZeta(a,s) + expZeta(-a,s))/2.

Русский

CosZeta равен среднему expZeta(a,s) и expZeta(-a,s): cosZeta(a,s) = (expZeta(a,s) + expZeta(-a,s))/2.

LaTeX

$$$$\\cosZeta(a,s) = \\frac{\\expZeta(a,s) + \\expZeta(-a,s)}{2}.$$$$

Lean4

theorem cosZeta_eq (a : UnitAddCircle) (s : ℂ) : cosZeta a s = (expZeta a s + expZeta (-a) s) / 2 :=
  by
  rw [expZeta, expZeta, cosZeta_neg, sinZeta_neg]
  ring_nf

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