noncommProd_commute — Mathlib

English

If every f(x) commutes with a fixed y in β, then y commutes with the noncommutative product of all f(x) over s.

Русский

Если каждый f(x) коммутирует с фиксированным элементом y в β, тогда y коммутирует с некоммопродом всех f(x) над s.

LaTeX

$$$ (s : \mathrm{Finset} \; \alpha) \; (f : \alpha \to \beta) \; (comm) (y : \beta) (h : \forall x \in s, \mathrm{Commute} \; y \; (f x)) : \mathrm{Commute} \; y \; (s.noncommProd f comm)$$$

Lean4

@[to_additive]
theorem noncommProd_commute (s : Finset α) (f : α → β) (comm) (y : β) (h : ∀ x ∈ s, Commute y (f x)) :
    Commute y (s.noncommProd f comm) := by
  apply Multiset.noncommProd_commute
  intro y
  rw [Multiset.mem_map]
  rintro ⟨x, ⟨hx, rfl⟩⟩
  exact h x hx

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