commute_noncommPiCoprod — Mathlib

English

If m commutes with all φ_i x, then m commutes with the entire noncommPiCoprod.

Русский

Если m коммутирует со всеми образами φ_i x, то m коммутирует с целым noncommPiCoprod.

LaTeX

$$$\\forall m,\\forall i,\\forall x,\\ \\mathrm{Commute}(m, (ϕ i x)) \\Rightarrow \\mathrm{Commute}(m, \\mathrm{noncommPiCoprod } ϕ hcomm).$$$

Lean4

@[to_additive]
theorem commute_noncommPiCoprod {m : M} (comm : ∀ i (x : N i), Commute m ((ϕ i x))) (h : (i : ι) → N i) :
    Commute m (MonoidHom.noncommPiCoprod ϕ hcomm h) :=
  by
  dsimp only [MonoidHom.noncommPiCoprod, MonoidHom.coe_mk, OneHom.coe_mk]
  apply Finset.noncommProd_induction
  · exact fun x y ↦ Commute.mul_right
  · exact Commute.one_right _
  · exact fun x _ ↦ comm x (h x)

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