RingEquiv.unop_map_list_prod

theorem RingEquiv.unop_map_list_prod : ∀ {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (f : R ≃+* Sᵐᵒᵖ) (l : List R), (f l.prod).unop = (List.map (MulOpposite.unop ∘ ⇑f) l).reverse.prod

The theorem `RingEquiv.unop_map_list_prod` states that for any types `R` and `S`, given that both `R` and `S` are semirings, and given an isomorphism `f` from `R` to the opposite ring of `S` and a list of elements from `R`, the unop (unary operation) of the product of the list under the isomorphism `f` is equivalent to the product of the reversed list where each element is first mapped under `f` and then the unop operation is applied. Essentially, this theorem deals with the interaction between ring isomorphisms and product operations in the setting of the opposite ring.

More concisely: For any semirings R and S, an isomorphism f from R to the opposite ring of S, and a list xs of elements from R, the unary operation of the product of xs under f is equivalent to the product of the reversed list of elements mapped under f with their unary operations applied.