English
Let f be a ring equivalence into the opposite ring; for any list l, the unop of the image of the product equals the reverse product of the unop images: unop(f(l.prod)) = (l.map (unop ∘ f)).reverse.prod.
Русский
Пусть f — кольцевой эквивалент в противоположное кольцо; для любого списка l верно: unop(f(l.prod)) равно произведению в обратном порядке изображений: reverse(l.map (unop ∘ f)).prod.
LaTeX
$$$$ \mathrm{unop}\left(f\left(l.\mathrm{prod}\right)\right) = \left( l.map\left(\mathrm{unop} \circ f\right) \right)^{\text{rev}}.\mathrm{prod}. $$$$
Lean4
/-- An isomorphism into the opposite ring acts on the product by acting on the reversed elements -/
protected theorem unop_map_list_prod [Semiring R] [Semiring S] (f : R ≃+* Sᵐᵒᵖ) (l : List R) :
MulOpposite.unop (f l.prod) = (l.map (MulOpposite.unop ∘ f)).reverse.prod :=
unop_map_list_prod f l
