Λ₀_eq — Mathlib

English

Let P be a WeakFEPair and s any complex number. Then Λ₀(s) equals Λ(s) plus (1/s) f₀ plus (ε/(k − s)) g₀.

Русский

Пусть P — слабый FEP-пар. Тогда для любого комплексного числа s выполняется Λ₀(s) = Λ(s) + (1/s) f₀ + (ε/(k − s)) g₀.

LaTeX

$$$\\Lambda_0(s) = \\Lambda(s) + \\frac{1}{s} f_0 + \\frac{\\varepsilon}{k - s} g_0$$$

Lean4

theorem Λ₀_eq (s : ℂ) : P.Λ₀ s = P.Λ s + (1 / s) • P.f₀ + (P.ε / (P.k - s)) • P.g₀ :=
  by
  unfold Λ Λ₀
  abel

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