smul_iff — Mathlib

English

For nonzero c, LSeriesSummable (c • f) s is equivalent to LSeriesSummable f s.

Русский

Для ненулевого c сумма суммируемости L-Series после умножения на c эквивалентна суммируемости исходной f.

LaTeX

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

Lean4

theorem smul_iff {f : ℕ → ℂ} {c s : ℂ} (hc : c ≠ 0) : LSeriesSummable (c • f) s ↔ LSeriesSummable f s :=
  ⟨of_smul hc, smul c⟩

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