# Results about mapping big operators across ring equivalences #

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

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

source
theorem RingEquiv.map_multiset_prod {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] (f : R ≃+* S) (s : Multiset R) :
f s.prod = (Multiset.map (⇑f) s).prod
source
theorem RingEquiv.map_multiset_sum {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) (s : Multiset R) :
f s.sum = (Multiset.map (⇑f) s).sum
source
theorem RingEquiv.map_prod {α : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] (g : R ≃+* S) (f : α → R) (s : Finset α) :
g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x)
source
theorem RingEquiv.map_sum {α : Type u_1} {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (g : R ≃+* S) (f : α → R) (s : Finset α) :
g (∑ x ∈ s, f x) = ∑ x ∈ s, g (f x)