smul — Mathlib

English

If f has a summable L-series at s with sum a, then c • f has L-series sum c • a at s.

Русский

Если у f L-ряд суммируем, имеем сумму a; тогда c • f имеет сумму c • a в s.

LaTeX

$$$\forall f:\mathbb{N}\to\mathbb{C},\ c\in\mathbb{C},\ {s,a}\in\mathbb{C},\ LSeriesHasSum\,f\,s\,a \Rightarrow LSeriesHasSum\,(c\cdot f)\,s\,(c\cdot a)$$$

Lean4

theorem smul {f : ℕ → ℂ} (c : ℂ) {s a : ℂ} (hf : LSeriesHasSum f s a) : LSeriesHasSum (c • f) s (c * a) := by
  simpa [LSeriesHasSum, term_smul] using hf.const_smul c

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