# Results about mapping big operators across ring equivalences #

theorem RingEquiv.map_list_prod {R : Type u_2} {S : Type u_3} [] [] (f : R ≃+* S) (l : List R) :
f l.prod = (List.map (f) l).prod
theorem RingEquiv.map_list_sum {R : Type u_2} {S : Type u_3} [] [] (f : R ≃+* S) (l : List R) :
f l.sum = (List.map (f) l).sum
theorem RingEquiv.unop_map_list_prod {R : Type u_2} {S : Type u_3} [] [] (f : R ≃+* Sᵐᵒᵖ) (l : List R) :
(f l.prod).unop = (List.map (MulOpposite.unop f) l).reverse.prod

An isomorphism into the opposite ring acts on the product by acting on the reversed elements

theorem RingEquiv.map_multiset_prod {R : Type u_2} {S : Type u_3} [] [] (f : R ≃+* S) (s : ) :
f s.prod = (Multiset.map (f) s).prod
theorem RingEquiv.map_multiset_sum {R : Type u_2} {S : Type u_3} [] [] (f : R ≃+* S) (s : ) :
f s.sum = (Multiset.map (f) s).sum
theorem RingEquiv.map_prod {α : Type u_1} {R : Type u_2} {S : Type u_3} [] [] (g : R ≃+* S) (f : αR) (s : ) :
g (s.prod fun (x : α) => f x) = s.prod fun (x : α) => g (f x)
theorem RingEquiv.map_sum {α : Type u_1} {R : Type u_2} {S : Type u_3} [] [] (g : R ≃+* S) (f : αR) (s : ) :
g (s.sum fun (x : α) => f x) = s.sum fun (x : α) => g (f x)