list_sum_right — Mathlib

English

If an element a commutes with every element of a list l in a nonunital semiring, then a commutes with the sum of the list: Commute a l.sum.

Русский

Если элемент a commuting с каждым элементом списка l в неединичном полугруппе, тогда a commuting с суммой списка: Commute a l.sum.

LaTeX

$$$a \;\text{commutes with } l.sum$ given $\forall b\in l, \;Commute(a,b)$$$

Lean4

theorem list_sum_right (a : R) (l : List R) (h : ∀ b ∈ l, Commute a b) : Commute a l.sum := by
  induction l with
  | nil => exact Commute.zero_right _
  | cons x xs ih =>
    rw [List.sum_cons]
    exact (h _ mem_cons_self).add_right (ih fun j hj ↦ h _ <| mem_cons_of_mem _ hj)

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