list_prod_right — Mathlib

English

If y commutes with every element of a list l, then y commutes with the product of l.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem _root_.Commute.list_prod_right (l : List M) (y : M) (h : ∀ x ∈ l, Commute y x) : Commute y l.prod := by
  induction l with
  | nil => simp
  | cons z l IH =>
    rw [List.forall_mem_cons] at h
    rw [List.prod_cons]
    exact Commute.mul_right h.1 (IH h.2)

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