LFunction_neg_two_mul_nat_sub_one

English

For an odd Φ, the L-function vanishes at negative odd integers: L(Φ, -(2n) - 1) = 0 for all n.

Русский

Для нечетной Φ нули L-функции в отрицательных нечетных аргументах: L(Φ, -(2n) - 1) = 0.

LaTeX

$$$$L(\Phi, -(2n) - 1) = 0.$$$$

Lean4

/-- The L-function of an odd function vanishes at negative odd integers. -/
@[simp]
theorem LFunction_neg_two_mul_nat_sub_one (hΦ : Φ.Odd) (n : ℕ) : LFunction Φ (-(2 * n) - 1) = 0 := by
  simp only [LFunction_def_odd hΦ, hurwitzZetaOdd_neg_two_mul_nat_sub_one, mul_zero, ← neg_mul, sum_const_zero]

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