differentiable_Λ₀

Mathlib.NumberTheory.LSeries.AbstractFuncEq

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

English

The function Λ₀ is complex-differentiable (holomorphic).

Русский

Функция Λ₀ является комплексно-дифференцируемой (гоморфной).

LaTeX

$$$\\text{Differentiable}_{\\mathbb{C}}(\\Lambda_0)$$$

Lean4

theorem differentiable_Λ₀ : Differentiable ℂ P.Λ₀ :=
  P.toStrongFEPair.differentiable_Λ

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

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

Разделы

Аффилиация

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