English
For the trivial Dirichlet character modulo N and s ≠ 1, the L-function factors as the Riemann zeta-function multiplied by the Euler product over primes dividing N: L(s, triv mod N) = ζ(s) · ∏_{p ∣ N} (1 − p^{−s}).
Русский
Для тривиального символа Дирихле по модулю N и s ≠ 1 L(s, тривиальный) делится как ζ(s)·∏_{p|N}(1−p^{−s}).
LaTeX
$$$L(s,\text{triv mod }N) = \zeta(s) \cdot \prod_{p \mid N} (1 - p^{-s})$$$
Lean4
/-- The L function of the trivial Dirichlet character mod `N` is obtained from the Riemann
zeta function by multiplying with `∏ p ∈ N.primeFactors, (1 - (p : ℂ) ^ (-s))`. -/
theorem LFunctionTrivChar_eq_mul_riemannZeta {s : ℂ} (hs : s ≠ 1) :
LFunctionTrivChar N s = (∏ p ∈ N.primeFactors, (1 - (p : ℂ) ^ (-s))) * riemannZeta s :=
by
rw [← LFunction_modOne_eq (χ := 1), LFunctionTrivChar, ← changeLevel_one N.one_dvd, mul_comm]
convert LFunction_changeLevel N.one_dvd 1 (.inr hs) using 4 with p
rw [MulChar.one_apply <| isUnit_of_subsingleton _, one_mul]
