summable_mul_right_iff — Mathlib

English

If a ≠ 0, Summable (λ i, f i * a) L ⇔ Summable f L.

Русский

Для a ≠ 0, суммируема ли последовательность f(i) · a ⇔ суммируема сама f(i).

LaTeX

$$$(\forall a, a \neq 0) \Rightarrow \left( \text{Summable } (\lambda i, f(i) \cdot a) L \iff \text{Summable } f L \right)$$$

Lean4

theorem summable_mul_right_iff (h : a ≠ 0) : (Summable (fun i ↦ f i * a) L) ↔ Summable f L :=
  ⟨fun H ↦ by simpa only [mul_inv_cancel_right₀ h] using H.mul_right a⁻¹, fun H ↦ H.mul_right _⟩

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