summable_const_div_iff — Mathlib

English

If a ≠ 0, then the series ∑ (a / f(i)) is summable with respect to L if and only if ∑ (1 / f(i)) is summable with respect to L.

Русский

Пусть a ≠ 0. Тогда сумма ∑ (a / f(i)) сходится относительно L тогда и только тогда, когда сумма ∑ (1 / f(i)) сходится относительно L.

LaTeX

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

Lean4

theorem summable_const_div_iff (h : a ≠ 0) : (Summable (fun i ↦ a / f i) L) ↔ Summable (1 / f) L := by
  simpa only [div_eq_mul_inv, one_mul] using summable_mul_left_iff h

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