# Documentation

Mathlib.Algebra.BigOperators.RingEquiv

# Results about mapping big operators across ring equivalences #

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

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

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