LFunction_neg_two_mul_nat_add_one

English

For an even Dirichlet character χ and any n, LFunction χ (−2(n+1)) = 0.

Русский

Для чётного Dirichlet-персонажа χ и любого n: LFunction χ (−2(n+1)) = 0.

LaTeX

$$LFunction χ (−2(n+1)) = 0$$

Lean4

/-- The L-function of an even Dirichlet character vanishes at strictly negative even integers. -/
@[simp]
theorem LFunction_neg_two_mul_nat_add_one {χ : DirichletCharacter ℂ N} (hχ : Even χ) (n : ℕ) :
    LFunction χ (-(2 * (n + 1))) = 0 :=
  ZMod.LFunction_neg_two_mul_nat_add_one hχ.to_fun n

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