completedLFunction_const_mul — Mathlib

English

Multiplying Φ by a constant scales the completed L-function by the same constant.

Русский

Умножение Φ на константу масштабирует завершенную L-функцию на ту же константу.

LaTeX

$$$$\mathrm{completedLFunction}(a \cdot \Phi, s) = a \cdot \mathrm{completedLFunction}(\Phi, s).$$$$

Lean4

theorem completedLFunction_const_mul (a : ℂ) (Φ : ZMod N → ℂ) (s : ℂ) :
    completedLFunction (fun j ↦ a * Φ j) s = a * completedLFunction Φ s :=
  by
  simp only [completedLFunction, mul_add, mul_sum]
  congr with i <;> ring

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