const_div

Mathlib.Topology.Algebra.InfiniteSum.Ring

URI: https://scilib.ai/kg/mathlib#Summable.const_div

English

If Summable (i ↦ 1 / f i) L, then for every b, Summable (i ↦ b / f i) L.

Русский

Если ∑ 1/f(i) сходится, то для любого b серия b / f(i) сходится.

LaTeX

$$$\text{Summable } (\lambda i, 1/f(i))\ L \Rightarrow \forall b, \text{Summable } (\lambda i, b/f(i))\ L$$$

Lean4

theorem const_div (h : Summable (fun x ↦ 1 / f x) L) (b : α) : Summable (fun i ↦ b / f i) L :=
  (h.hasSum.const_div b).summable

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru