sum_left — Mathlib

English

If each f_i commutes with b, then the sum over i of f_i commutes with b.

Русский

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

LaTeX

$$$$ \\text{Commute} \\Big( \\sum_{i\\in s} f_i, \\; b \\Big). $$$$

Lean4

theorem _root_.Commute.sum_left (s : Finset ι) (f : ι → R) (b : R) (h : ∀ i ∈ s, Commute (f i) b) :
    Commute (∑ i ∈ s, f i) b :=
  ((Commute.sum_right _ _ _) fun _i hi => (h _ hi).symm).symm

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