LFunction_neg_two_mul_nat_sub_one

English

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

Русский

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

LaTeX

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

Lean4

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

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