gammaFactor_def

Mathlib.NumberTheory.LSeries.DirichletContinuation

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

English

If χ is odd, then gammaFactor χ s = Γℝ(s+1).

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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