div_const

Mathlib.Topology.Algebra.InfiniteSum.Ring

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

English

If HasSum f a with respect to L, 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 : HasSum f a L) (b : α) : HasSum (fun i ↦ f i / b) (a / b) L := by
  simp only [div_eq_mul_inv, h.mul_right b⁻¹]

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

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

Разделы

Аффилиация

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