tsum_left

Mathlib.Topology.Algebra.InfiniteSum.Ring

URI: https://scilib.ai/kg/mathlib#Commute.tsum_left

English

If each f(i) commutes with a, then the sum commutes with a on the left: a commutes with ∑ f(i).

Русский

Если все f(i) коммутируют с a слева, то сумма также коммутирует с a слева.

LaTeX

$$$\forall i,\ Commute (f(i)) a \Rightarrow Commute (\sum' i, f(i)) a$$$

Lean4

theorem tsum_left (a) (h : ∀ i, Commute (f i) a) : Commute (∑'[L] i, f i) a :=
  (Commute.tsum_right _ fun i ↦ (h i).symm).symm

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

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

Разделы

Аффилиация

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