completedLFunction_zero — Mathlib

English

The completed L-function vanishes for the zero input function: completedLFunction 0 s = 0.

Русский

Завершенная L-функция для нулевой функции равна нулю: completedLFunction 0 s = 0.

LaTeX

$$$$completedLFunction(0, s) = 0.$$$$

Lean4

@[simp]
theorem completedLFunction_zero (s : ℂ) : completedLFunction (0 : ZMod N → ℂ) s = 0 := by
  simp only [completedLFunction, Pi.zero_apply, zero_mul, sum_const_zero, mul_zero, zero_add]

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