smul — Mathlib

English

If f is L-series summable at s, then any scalar multiple c • f is summable at s.

Русский

Если f суммируема в L-ряд на s, то любое слагаемое множитель c • f суммируемо на s.

LaTeX

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

Lean4

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

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