LSeries_smul — Mathlib

English

The L-series respects scalar multiplication: LSeries (c • f) s = c • LSeries f s for any f, c, s.

Русский

L-ряд сохраняет скаляpное умножение: LSeries (c • f) s = c • LSeries f s.

LaTeX

$$$\forall f:\mathbb{N}\to\mathbb{C},\ c,s\in\mathbb{C},\ LSeries\,(c\cdot f)\,s = c\cdot LSeries\,f\,s$$$

Lean4

@[simp]
theorem LSeries_smul (f : ℕ → ℂ) (c s : ℂ) : LSeries (c • f) s = c * LSeries f s := by
  simp [LSeries, term_smul_apply, tsum_mul_left]

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