# mathlib3documentation

algebra.big_operators.ring_equiv

# Results about mapping big operators across ring equivalences #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected]
theorem ring_equiv.map_list_prod {R : Type u_2} {S : Type u_3} [semiring R] [semiring S] (f : R ≃+* S) (l : list R) :
f l.prod = l).prod
@[protected]
theorem ring_equiv.map_list_sum {R : Type u_2} {S : Type u_3} (f : R ≃+* S) (l : list R) :
f l.sum = l).sum
@[protected]
theorem ring_equiv.unop_map_list_prod {R : Type u_2} {S : Type u_3} [semiring R] [semiring S] (f : R ≃+* Sᵐᵒᵖ) (l : list R) :

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

@[protected]
theorem ring_equiv.map_multiset_prod {R : Type u_2} {S : Type u_3} (f : R ≃+* S) (s : multiset R) :
f s.prod = s).prod
@[protected]
theorem ring_equiv.map_multiset_sum {R : Type u_2} {S : Type u_3} (f : R ≃+* S) (s : multiset R) :
f s.sum = s).sum
@[protected]
theorem ring_equiv.map_prod {α : Type u_1} {R : Type u_2} {S : Type u_3} (g : R ≃+* S) (f : α R) (s : finset α) :
g (s.prod (λ (x : α), f x)) = s.prod (λ (x : α), g (f x))
@[protected]
theorem ring_equiv.map_sum {α : Type u_1} {R : Type u_2} {S : Type u_3} (g : R ≃+* S) (f : α R) (s : finset α) :
g (s.sum (λ (x : α), f x)) = s.sum (λ (x : α), g (f x))