list_prod_left — Mathlib

English

If every element of l commutes with y, then l.prod commutes with y.

Русский

Если каждый элемент списка l коммутирует с y, тогда произведение списка коммутирует с y.

LaTeX

$$$ (\forall x \in l, Commute x y) \Rightarrow Commute l.prod y $$$

Lean4

@[to_additive]
theorem _root_.Commute.list_prod_left (l : List M) (y : M) (h : ∀ x ∈ l, Commute x y) : Commute l.prod y :=
  ((Commute.list_prod_right _ _) fun _ hx => (h _ hx).symm).symm

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