English
If we map a Monoid hom g through a noncommutative product, it commutes with the image product and respects the commutation structure transported by g.
Русский
Если мы отображаем некоммопрод через однородную гомоморфизм g, то гомоморфизм сохраняет структуру некоммопродукта и переносит коммутативность.
LaTeX
$$$ [MonoidHomClass F \beta \gamma] (s : \mathrm{Finset} \; \alpha) (f : \alpha \to \beta) (comm : s.\mathrm{toSet}.Pairwise (\mathrm{Commute} \; on \; f)) (g : F) \\; g (s.noncommProd f comm) = s.noncommProd (fun i => g (f i)) (fun _ hx _ hy _ => (comm.of_refl hx hy).map g)$$$
Lean4
@[to_additive]
theorem map_noncommProd [MonoidHomClass F β γ] (s : Finset α) (f : α → β) (comm) (g : F) :
g (s.noncommProd f comm) = s.noncommProd (fun i => g (f i)) fun _ hx _ hy _ => (comm.of_refl hx hy).map g := by
simp [noncommProd, Multiset.map_noncommProd]
