LFunctionTrivChar — Mathlib

English

The L-function associated to the trivial Dirichlet character modulo N is the standard Dirichlet L-function of the trivial character, i.e., L(s, triv mod N) is defined as the L-function of the constant-1 Dirichlet character modulo N.

Русский

L-функция, связанная с тривиальным символом Дирихле по модулю N, есть обычная L-функция тривиального символа по модулю N.

LaTeX

$$$L\text{FunctionTrivChar}(N,s) = L(\chi_{0},s)\quad\text{for }\chi_{0}\text{ тривиальный по модулю }N$$$

Lean4

/-- The `L`-function of the trivial character mod `N`. -/
noncomputable abbrev LFunctionTrivChar (N : ℕ) [NeZero N] :=
  (1 : DirichletCharacter ℂ N).LFunction

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