summable_div_const_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 \big( \text{Summable } (\lambda i, f(i)/a) L \iff \text{Summable } f L \big)$$$

Lean4

theorem summable_div_const_iff (h : a ≠ 0) : (Summable (fun i ↦ f i / a) L) ↔ Summable f L := by
  simpa only [div_eq_mul_inv] using summable_mul_right_iff (inv_ne_zero h)

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