LSeries_modOne_eq

Mathlib.NumberTheory.LSeries.Dirichlet

URI: https://scilib.ai/kg/mathlib#DirichletCharacter.LSeries_modOne_eq

English

The L-series associated to the mod-1 character equals the L-series of the constant sequence 1: L(χ1) = L(1).

Русский

Л-ряд, связанный с χ модуля 1, равен L-процессу константы 1: L(χ1) = L(1).

LaTeX

$$$L(\uparrow χ_1) = L(1).$$$

Lean4

theorem LSeries_modOne_eq : L ↗χ₁ = L 1 :=
  congr_arg L modOne_eq_one

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

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

Разделы

Аффилиация

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