tsum_mul_right

Mathlib.Topology.Algebra.InfiniteSum.Ring

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

English

In a suitable topological semiring, ∑' i, f i * a = (∑' i, f i) * a.

Русский

В подходящей топологической полуалгебре выполняется ∑' i, f(i) · a = (∑' i, f(i)) · a.

LaTeX

$$$\text{tsum}_{i\in L}(f(i) \cdot a) = \text{tsum}_{i\in L}(f(i)) \cdot a$$$

Lean4

protected theorem tsum_mul_right (a) (hf : Summable f L) : ∑'[L] i, f i * a = (∑'[L] i, f i) * a :=
  (hf.hasSum.mul_right _).tsum_eq

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

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

Разделы

Аффилиация

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