Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+βCtrl+βto navigate, Ctrl+π±οΈto focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Johannes HΓΆlzl, Callum Sutton, Yury Kudryashov

! This file was ported from Lean 3 source module algebra.big_operators.ring_equiv
! leanprover-community/mathlib commit 008205aa645b3f194c1da47025c5f110c8406eab
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Algebra.Ring.Equiv

/-!
# Results about mapping big operators across ring equivalences
-/

namespace RingEquiv

open BigOperators

variable {Ξ±: Type ?u.28950Ξ± R: Type ?u.14R S: Type ?u.8S : Type _: Type (?u.58338+1)Type _}

protected theorem map_list_prod: β [inst : Semiring R] [inst_1 : Semiring S] (f : R β+* S) (l : List R), βf (List.prod l) = List.prod (List.map (βf) l)map_list_prod [Semiring: Type ?u.20 β Type ?u.20Semiring R: Type ?u.14R] [Semiring: Type ?u.23 β Type ?u.23Semiring S: Type ?u.17S] (f: R β+* Sf : R: Type ?u.14R β+* S: Type ?u.17S) (l: List Rl : List: Type ?u.430 β Type ?u.430List R: Type ?u.14R) :
f: R β+* Sf l: List Rl.prod: {Ξ± : Type ?u.7187} β [inst : Mul Ξ±] β [inst : One Ξ±] β List Ξ± β Ξ±prod = (l: List Rl.map: {Ξ± : Type ?u.7221} β {Ξ² : Type ?u.7220} β (Ξ± β Ξ²) β List Ξ± β List Ξ²map f: R β+* Sf).prod: {Ξ± : Type ?u.13954} β [inst : Mul Ξ±] β [inst : One Ξ±] β List Ξ± β Ξ±prod := map_list_prod: β {M : Type ?u.13995} {N : Type ?u.13996} [inst : Monoid M] [inst_1 : Monoid N] {F : Type ?u.13994}
[inst_2 : MonoidHomClass F M N] (f : F) (l : List M), βf (List.prod l) = List.prod (List.map (βf) l)map_list_prod f: R β+* Sf l: List Rl
#align ring_equiv.map_list_prod RingEquiv.map_list_prod: β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R β+* S) (l : List R),
βf (List.prod l) = List.prod (List.map (βf) l)RingEquiv.map_list_prod

protected theorem map_list_sum: β {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R β+* S) (l : List R),
βf (List.sum l) = List.sum (List.map (βf) l)map_list_sum [NonAssocSemiring: Type ?u.14267 β Type ?u.14267NonAssocSemiring R: Type ?u.14261R] [NonAssocSemiring: Type ?u.14270 β Type ?u.14270NonAssocSemiring S: Type ?u.14264S] (f: R β+* Sf : R: Type ?u.14261R β+* S: Type ?u.14264S)
(l: List Rl : List: Type ?u.14645 β Type ?u.14645List R: Type ?u.14261R) : f: R β+* Sf l: List Rl.sum: {Ξ± : Type ?u.21402} β [inst : Add Ξ±] β [inst : Zero Ξ±] β List Ξ± β Ξ±sum = (l: List Rl.map: {Ξ± : Type ?u.21620} β {Ξ² : Type ?u.21619} β (Ξ± β Ξ²) β List Ξ± β List Ξ²map f: R β+* Sf).sum: {Ξ± : Type ?u.28353} β [inst : Add Ξ±] β [inst : Zero Ξ±] β List Ξ± β Ξ±sum := map_list_sum: β {M : Type ?u.28578} {N : Type ?u.28579} [inst : AddMonoid M] [inst_1 : AddMonoid N] {F : Type ?u.28577}
[inst_2 : AddMonoidHomClass F M N] (f : F) (l : List M), βf (List.sum l) = List.sum (List.map (βf) l)map_list_sum f: R β+* Sf l: List Rl
#align ring_equiv.map_list_sum RingEquiv.map_list_sum: β {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R β+* S) (l : List R),
βf (List.sum l) = List.sum (List.map (βf) l)RingEquiv.map_list_sum

/-- An isomorphism into the opposite ring acts on the product by acting on the reversed elements -/
protected theorem unop_map_list_prod: β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R β+* Sα΅α΅α΅) (l : List R),
MulOpposite.unop (βf (List.prod l)) = List.prod (List.reverse (List.map (MulOpposite.unop β βf) l))unop_map_list_prod [Semiring: Type ?u.28959 β Type ?u.28959Semiring R: Type ?u.28953R] [Semiring: Type ?u.28962 β Type ?u.28962Semiring S: Type ?u.28956S] (f: R β+* Sα΅α΅α΅f : R: Type ?u.28953R β+* S: Type ?u.28956Sα΅α΅α΅) (l: List Rl : List: Type ?u.29387 β Type ?u.29387List R: Type ?u.28953R) :
MulOpposite.unop: {Ξ± : Type ?u.29391} β Ξ±α΅α΅α΅ β Ξ±MulOpposite.unop (f: R β+* Sα΅α΅α΅f l: List Rl.prod: {Ξ± : Type ?u.36146} β [inst : Mul Ξ±] β [inst : One Ξ±] β List Ξ± β Ξ±prod) = (l: List Rl.map: {Ξ± : Type ?u.36182} β {Ξ² : Type ?u.36181} β (Ξ± β Ξ²) β List Ξ± β List Ξ²map (MulOpposite.unop: {Ξ± : Type ?u.36197} β Ξ±α΅α΅α΅ β Ξ±MulOpposite.unop β f: R β+* Sα΅α΅α΅f)).reverse: {Ξ± : Type ?u.42931} β List Ξ± β List Ξ±reverse.prod: {Ξ± : Type ?u.42934} β [inst : Mul Ξ±] β [inst : One Ξ±] β List Ξ± β Ξ±prod :=
unop_map_list_prod: β {M : Type ?u.43057} {N : Type ?u.43058} [inst : Monoid M] [inst_1 : Monoid N] {F : Type ?u.43056}
[inst_2 : MonoidHomClass F M Nα΅α΅α΅] (f : F) (l : List M),
MulOpposite.unop (βf (List.prod l)) = List.prod (List.reverse (List.map (MulOpposite.unop β βf) l))unop_map_list_prod f: R β+* Sα΅α΅α΅f l: List Rl
#align ring_equiv.unop_map_list_prod RingEquiv.unop_map_list_prod: β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R β+* Sα΅α΅α΅) (l : List R),
MulOpposite.unop (βf (List.prod l)) = List.prod (List.reverse (List.map (MulOpposite.unop β βf) l))RingEquiv.unop_map_list_prod

protected theorem map_multiset_prod: β {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R β+* S) (s : Multiset R),
βf (Multiset.prod s) = Multiset.prod (Multiset.map (βf) s)map_multiset_prod [CommSemiring: Type ?u.43401 β Type ?u.43401CommSemiring R: Type ?u.43395R] [CommSemiring: Type ?u.43404 β Type ?u.43404CommSemiring S: Type ?u.43398S] (f: R β+* Sf : R: Type ?u.43395R β+* S: Type ?u.43398S)
(s: Multiset Rs : Multiset: Type ?u.44047 β Type ?u.44047Multiset R: Type ?u.43395R) : f: R β+* Sf s: Multiset Rs.prod: {Ξ± : Type ?u.50804} β [inst : CommMonoid Ξ±] β Multiset Ξ± β Ξ±prod = (s: Multiset Rs.map: {Ξ± : Type ?u.50903} β {Ξ² : Type ?u.50902} β (Ξ± β Ξ²) β Multiset Ξ± β Multiset Ξ²map f: R β+* Sf).prod: {Ξ± : Type ?u.57636} β [inst : CommMonoid Ξ±] β Multiset Ξ± β Ξ±prod :=
map_multiset_prod: β {Ξ± : Type ?u.57741} {Ξ² : Type ?u.57742} [inst : CommMonoid Ξ±] [inst_1 : CommMonoid Ξ²] {F : Type ?u.57743}
[inst_2 : MonoidHomClass F Ξ± Ξ²] (f : F) (s : Multiset Ξ±), βf (Multiset.prod s) = Multiset.prod (Multiset.map (βf) s)map_multiset_prod f: R β+* Sf s: Multiset Rs
#align ring_equiv.map_multiset_prod RingEquiv.map_multiset_prod: β {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R β+* S) (s : Multiset R),
βf (Multiset.prod s) = Multiset.prod (Multiset.map (βf) s)RingEquiv.map_multiset_prod

protected theorem map_multiset_sum: β {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R β+* S)
(s : Multiset R), βf (Multiset.sum s) = Multiset.sum (Multiset.map (βf) s)map_multiset_sum [NonAssocSemiring: Type ?u.58347 β Type ?u.58347NonAssocSemiring R: Type ?u.58341R] [NonAssocSemiring: Type ?u.58350 β Type ?u.58350NonAssocSemiring S: Type ?u.58344S] (f: R β+* Sf : R: Type ?u.58341R β+* S: Type ?u.58344S)
(s: Multiset Rs : Multiset: Type ?u.58725 β Type ?u.58725Multiset R: Type ?u.58341R) : f: R β+* Sf s: Multiset Rs.sum: {Ξ± : Type ?u.65482} β [inst : AddCommMonoid Ξ±] β Multiset Ξ± β Ξ±sum = (s: Multiset Rs.map: {Ξ± : Type ?u.65699} β {Ξ² : Type ?u.65698} β (Ξ± β Ξ²) β Multiset Ξ± β Multiset Ξ²map f: R β+* Sf).sum: {Ξ± : Type ?u.72432} β [inst : AddCommMonoid Ξ±] β Multiset Ξ± β Ξ±sum :=
map_multiset_sum: β {Ξ± : Type ?u.72655} {Ξ² : Type ?u.72656} [inst : AddCommMonoid Ξ±] [inst_1 : AddCommMonoid Ξ²] {F : Type ?u.72657}
[inst_2 : AddMonoidHomClass F Ξ± Ξ²] (f : F) (s : Multiset Ξ±), βf (Multiset.sum s) = Multiset.sum (Multiset.map (βf) s)map_multiset_sum f: R β+* Sf s: Multiset Rs
#align ring_equiv.map_multiset_sum RingEquiv.map_multiset_sum: β {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R β+* S)
(s : Multiset R), βf (Multiset.sum s) = Multiset.sum (Multiset.map (βf) s)RingEquiv.map_multiset_sum

protected theorem map_prod: β {Ξ± : Type u_3} {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (g : R β+* S)
(f : Ξ± β R) (s : Finset Ξ±), βg (β x in s, f x) = β x in s, βg (f x)map_prod [CommSemiring: Type ?u.73322 β Type ?u.73322CommSemiring R: Type ?u.73316R] [CommSemiring: Type ?u.73325 β Type ?u.73325CommSemiring S: Type ?u.73319S] (g: R β+* Sg : R: Type ?u.73316R β+* S: Type ?u.73319S) (f: Ξ± β Rf : Ξ±: Type ?u.73313Ξ± β R: Type ?u.73316R)
(s: Finset Ξ±s : Finset: Type ?u.73972 β Type ?u.73972Finset Ξ±: Type ?u.73313Ξ±) : g: R β+* Sg (β x: ?m.80761x in s: Finset Ξ±s, f: Ξ± β Rf x: ?m.80761x) = β x: ?m.80863x in s: Finset Ξ±s, g: R β+* Sg (f: Ξ± β Rf x: ?m.80863x) :=
map_prod: β {Ξ² : Type ?u.87692} {Ξ± : Type ?u.87691} {Ξ³ : Type ?u.87690} [inst : CommMonoid Ξ²] [inst_1 : CommMonoid Ξ³]
{G : Type ?u.87693} [inst_2 : MonoidHomClass G Ξ² Ξ³] (g : G) (f : Ξ± β Ξ²) (s : Finset Ξ±),
βg (β x in s, f x) = β x in s, βg (f x)map_prod g: R β+* Sg f: Ξ± β Rf s: Finset Ξ±s
#align ring_equiv.map_prod RingEquiv.map_prod: β {Ξ± : Type u_3} {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (g : R β+* S)
(f : Ξ± β R) (s : Finset Ξ±), βg (β x in s, f x) = β x in s, βg (f x)RingEquiv.map_prod

protected theorem map_sum: β {Ξ± : Type u_3} {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (g : R β+* S)
(f : Ξ± β R) (s : Finset Ξ±), βg (β x in s, f x) = β x in s, βg (f x)map_sum [NonAssocSemiring: Type ?u.88303 β Type ?u.88303NonAssocSemiring R: Type ?u.88297R] [NonAssocSemiring: Type ?u.88306 β Type ?u.88306NonAssocSemiring S: Type ?u.88300S] (g: R β+* Sg : R: Type ?u.88297R β+* S: Type ?u.88300S) (f: Ξ± β Rf : Ξ±: Type ?u.88294Ξ± β R: Type ?u.88297R)
(s: Finset Ξ±s : Finset: Type ?u.88685 β Type ?u.88685Finset Ξ±: Type ?u.88294Ξ±) : g: R β+* Sg (β x: ?m.95475x in s: Finset Ξ±s, f: Ξ± β Rf x: ?m.95475x) = β x: ?m.95695x in s: Finset Ξ±s, g: R β+* Sg (f: Ξ± β Rf x: ?m.95695x) :=
map_sum: β {Ξ² : Type ?u.102642} {Ξ± : Type ?u.102641} {Ξ³ : Type ?u.102640} [inst : AddCommMonoid Ξ²] [inst_1 : AddCommMonoid Ξ³]
{G : Type ?u.102643} [inst_2 : AddMonoidHomClass G Ξ² Ξ³] (g : G) (f : Ξ± β Ξ²) (s : Finset Ξ±),
βg (β x in s, f x) = β x in s, βg (f x)map_sum g: R β+* Sg f: Ξ± β Rf s: Finset Ξ±s
#align ring_equiv.map_sum RingEquiv.map_sum: β {Ξ± : Type u_3} {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (g : R β+* S)
(f : Ξ± β R) (s : Finset Ξ±), βg (β x in s, f x) = β x in s, βg (f x)RingEquiv.map_sum

end RingEquiv
```