gammaFactor_def

Mathlib.NumberTheory.LSeries.DirichletContinuation

URI: https://scilib.ai/kg/mathlib#DirichletCharacter.Even.gammaFactor_def

English

If χ is even, then gammaFactor χ s = Γℝ s.

Русский

Если χ чётный, то gammaFactor χ s = Γℝ(s).

LaTeX

$$$\gamma\text{Factor}(\chi,s) = \Gamma_{\mathbb{R}}(s)\quad(\chi\text{ чётный})$$$

Lean4

theorem gammaFactor_def {χ : DirichletCharacter ℂ N} (hχ : χ.Even) (s : ℂ) : gammaFactor χ s = Gammaℝ s := by
  simp [gammaFactor, hχ]

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

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

Разделы

Аффилиация

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