div_const

Mathlib.Topology.Algebra.InfiniteSum.Ring

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

English

If HasSum f a, then HasSum (i ↦ f(i) / b) (a / b) for any b.

Русский

Если сумма f равна a, то сумма f(i)/b равна a/b.

LaTeX

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

Lean4

theorem div_const (h : Summable f L) (b : α) : Summable (fun i ↦ f i / b) L :=
  (h.hasSum.div_const _).summable

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

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

Разделы

Аффилиация

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