multiset_sum_left — Mathlib

English

Let s be a finite multiset of a nonunital nonassoc semiring. If every element b ∈ s commutes with a, then a commutes with s.sum: (s.sum) a = a (s.sum).

Русский

Пусть s — конечное мультимножество в полусистеме без единицы и без ассоциативности. Если каждый элемент b ∈ s commute с a, то сумма s.commutes с a: (s.sum) a = a (s.sum).

LaTeX

$$$$ (\\forall b \\in s,\\ a b = b a) \\Rightarrow \\left( \\left( \\sum_{b \\in s} b \\right) a = a \\left( \\sum_{b \in s} b \\right) \\right). $$$$

Lean4

theorem multiset_sum_left (b : R) (h : ∀ a ∈ s, Commute a b) : Commute s.sum b :=
  ((Commute.multiset_sum_right _ _) fun _ ha => (h _ ha).symm).symm

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