tsum_mul_right — Mathlib

English

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

Русский

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

LaTeX

$$$[T2Space \alpha] \Rightarrow \sum' i, f(i) \cdot a = (\sum' i, f(i)) \cdot a$$$

Lean4

theorem tsum_mul_right [T2Space α] : ∑'[L] x, f x * a = (∑'[L] x, f x) * a :=
  by
  by_cases ha : a = 0
  · simp [ha]
  · exact ((Homeomorph.mulRight₀ a ha).isClosedEmbedding.map_tsum f (g := AddMonoidHom.mulRight a)).symm

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