noncommProd_commute — Mathlib

English

If every x in s commutes with y, then y commutes with the entire noncommProd comm of s.

Русский

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

LaTeX

$$$\\forall s,\\; comm,\\; y:\\alpha,\\; (\\forall x\\in s, Commute\\ y\\ x) \\Rightarrow Commute\\ y\\ (s.noncommProd comm)$$$

Lean4

@[to_additive]
theorem noncommProd_commute (s : Multiset α) (comm) (y : α) (h : ∀ x ∈ s, Commute y x) :
    Commute y (s.noncommProd comm) := by
  induction s using Quotient.inductionOn
  simp only [quot_mk_to_coe, noncommProd_coe]
  exact Commute.list_prod_right _ _ h

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