English
Let F be a type with FunLike structure and a MonoidHomClass to Mᵐᵒᵖ. For a map f, the unop of f applied to the product equals the reverse-ordered product of unops of f on the elements: (f(l.prod)).unop = (l.map (unop ∘ f)).reverse.prod.
Русский
Пусть F обладает структурой FunLike, и существует гомоморфизм Моноида в противоположный. ТогдаUnop(f(l.prod)) = prod( reverse( map(unop ∘ f) l) ).
LaTeX
$$$ (f\, l).{\mathrm{unop}} = \mathrm{prod}(\mathrm{reverse}(\mathrm{map}(\mathrm{unop} \circ f)\, l)) $$$
Lean4
/-- A morphism into the opposite monoid acts on the product by acting on the reversed elements. -/
theorem unop_map_list_prod {F : Type*} [FunLike F M Nᵐᵒᵖ] [MonoidHomClass F M Nᵐᵒᵖ] (f : F) (l : List M) :
(f l.prod).unop = (l.map (MulOpposite.unop ∘ f)).reverse.prod := by
rw [map_list_prod f l, MulOpposite.unop_list_prod, List.map_map]
