sum_right — Mathlib

English

If a fixed element b commutes with every f_i, then b commutes with the sum over i of f_i.

Русский

Если фиксированный элемент b коммутирует с каждым f_i, то он коммутирует с суммой по i from f_i.

LaTeX

$$$$ \\text{Commute } b \\left( \\sum_{i\\in s} f_i \\right). $$$$

Lean4

theorem _root_.Commute.sum_right (s : Finset ι) (f : ι → R) (b : R) (h : ∀ i ∈ s, Commute b (f i)) :
    Commute b (∑ i ∈ s, f i) :=
  (Commute.multiset_sum_right _ _) fun b hb =>
    by
    obtain ⟨i, hi, rfl⟩ := Multiset.mem_map.mp hb
    exact h _ hi

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