English
For a map f that is a MonoidHomClass between α and β, the image of the noncommProd of s equals the noncommProd of the mapped elements, up to a corresponding auxiliary commutativity witness.
Русский
При отображении f, являющемся гомоморфизмом моноидов, образ noncommProd(s) равен noncommProd отображённых элементов с соответствующим вспомогательным доказательством коммутативности.
LaTeX
$$$f\\left( s.noncommProd comm\\right) = (s.map f).noncommProd (\\text{map\\_noncommProd\_aux } s comm f)$$$
Lean4
@[to_additive]
theorem map_noncommProd [MonoidHomClass F α β] (s : Multiset α) (comm) (f : F) :
f (s.noncommProd comm) = (s.map f).noncommProd (Multiset.map_noncommProd_aux s comm f) :=
by
induction s using Quotient.inductionOn
simpa using map_list_prod f _
