multiset_sum_right — Mathlib

English

Let s be a finite multiset of a nonunital nonassoc semiring, and b an element with the property that every element of s commutes with b. Then the sum s.sum commutes with b: (s.sum) b = b (s.sum).

Русский

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

LaTeX

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

Lean4

theorem multiset_sum_right (a : R) (h : ∀ b ∈ s, Commute a b) : Commute a s.sum :=
  by
  induction s using Quotient.inductionOn
  rw [quot_mk_to_coe, sum_coe]
  exact Commute.list_sum_right _ _ h

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