functional_equation₀

Mathlib.NumberTheory.LSeries.AbstractFuncEq

URI: https://scilib.ai/kg/mathlib#WeakFEPair.functional_equation₀

← MathLib Explorer

English

The functional equation for Λ₀ holds: Λ₀(k − s) = ε · symm.Λ₀(s).

Русский

Функциональное уравнение для Λ₀: Λ₀(k − s) = ε · Λ₀^{symm}(s).

LaTeX

$$$\\Lambda_0(k - s) = \\varepsilon \\cdot \\Lambda_0^{\\mathrm{symm}}(s)$$$

Lean4

/-- Functional equation formulated for `Λ₀`. -/
theorem functional_equation₀ (s : ℂ) : P.Λ₀ (P.k - s) = P.ε • P.symm.Λ₀ s :=
  P.toStrongFEPair.functional_equation s

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru