/-
Copyright (c) 2018 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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.14
R 
S: Type ?u.8
S : 
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.20
Semiring 
R: Type ?u.14
R] [
Semiring: Type ?u.23 → Type ?u.23
Semiring 
S: Type ?u.17
S] (
f: R ≃+* S
f : 
R: Type ?u.14
R ≃+* 
S: Type ?u.17
S) (
l: List R
l : 
List: Type ?u.430 → Type ?u.430
List 
R: Type ?u.14
R) :
    
f: R ≃+* S
f 
l: List R
l.
prod: {α : Type ?u.7187} → [inst : Mul α] → [inst : One α] → List α → α
prod = (
l: List R
l.
map: {α : Type ?u.7221} → {β : Type ?u.7220} → (α → β) → List α → List β
map 
f: R ≃+* S
f).
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 ≃+* S
f 
l: List R
l
#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.14267
NonAssocSemiring 
R: Type ?u.14261
R] [
NonAssocSemiring: Type ?u.14270 → Type ?u.14270
NonAssocSemiring 
S: Type ?u.14264
S] (
f: R ≃+* S
f : 
R: Type ?u.14261
R ≃+* 
S: Type ?u.14264
S)
    (
l: List R
l : 
List: Type ?u.14645 → Type ?u.14645
List 
R: Type ?u.14261
R) : 
f: R ≃+* S
f 
l: List R
l.
sum: {α : Type ?u.21402} → [inst : Add α] → [inst : Zero α] → List α → α
sum = (
l: List R
l.
map: {α : Type ?u.21620} → {β : Type ?u.21619} → (α → β) → List α → List β
map 
f: R ≃+* S
f).
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 ≃+* S
f 
l: List R
l
#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.28959
Semiring 
R: Type ?u.28953
R] [
Semiring: Type ?u.28962 → Type ?u.28962
Semiring 
S: Type ?u.28956
S] (
f: R ≃+* Sᵐᵒᵖ
f : 
R: Type ?u.28953
R ≃+* 
S: Type ?u.28956
Sᵐᵒᵖ) (
l: List R
l : 
List: Type ?u.29387 → Type ?u.29387
List 
R: Type ?u.28953
R) :
    
MulOpposite.unop: {α : Type ?u.29391} → αᵐᵒᵖ → α
MulOpposite.unop (
f: R ≃+* Sᵐᵒᵖ
f 
l: List R
l.
prod: {α : Type ?u.36146} → [inst : Mul α] → [inst : One α] → List α → α
prod) = (
l: List R
l.
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 R
l
#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.43401
CommSemiring 
R: Type ?u.43395
R] [
CommSemiring: Type ?u.43404 → Type ?u.43404
CommSemiring 
S: Type ?u.43398
S] (
f: R ≃+* S
f : 
R: Type ?u.43395
R ≃+* 
S: Type ?u.43398
S)
    (
s: Multiset R
s : 
Multiset: Type ?u.44047 → Type ?u.44047
Multiset 
R: Type ?u.43395
R) : 
f: R ≃+* S
f 
s: Multiset R
s.
prod: {α : Type ?u.50804} → [inst : CommMonoid α] → Multiset α → α
prod = (
s: Multiset R
s.
map: {α : Type ?u.50903} → {β : Type ?u.50902} → (α → β) → Multiset α → Multiset β
map 
f: R ≃+* S
f).
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 ≃+* S
f 
s: Multiset R
s
#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.58347
NonAssocSemiring 
R: Type ?u.58341
R] [
NonAssocSemiring: Type ?u.58350 → Type ?u.58350
NonAssocSemiring 
S: Type ?u.58344
S] (
f: R ≃+* S
f : 
R: Type ?u.58341
R ≃+* 
S: Type ?u.58344
S)
    (
s: Multiset R
s : 
Multiset: Type ?u.58725 → Type ?u.58725
Multiset 
R: Type ?u.58341
R) : 
f: R ≃+* S
f 
s: Multiset R
s.
sum: {α : Type ?u.65482} → [inst : AddCommMonoid α] → Multiset α → α
sum = (
s: Multiset R
s.
map: {α : Type ?u.65699} → {β : Type ?u.65698} → (α → β) → Multiset α → Multiset β
map 
f: R ≃+* S
f).
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 ≃+* S
f 
s: Multiset R
s
#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.73322
CommSemiring 
R: Type ?u.73316
R] [
CommSemiring: Type ?u.73325 → Type ?u.73325
CommSemiring 
S: Type ?u.73319
S] (
g: R ≃+* S
g : 
R: Type ?u.73316
R ≃+* 
S: Type ?u.73319
S) (
f: α → R
f : 
α: Type ?u.73313
α → 
R: Type ?u.73316
R)
    (
s: Finset α
s : 
Finset: Type ?u.73972 → Type ?u.73972
Finset 
α: Type ?u.73313
α) : 
g: R ≃+* S
g (∏ 
x: ?m.80761
x in 
s: Finset α
s, 
f: α → R
f 
x: ?m.80761
x) = ∏ 
x: ?m.80863
x in 
s: Finset α
s, 
g: R ≃+* S
g (
f: α → R
f 
x: ?m.80863
x) :=
  
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 ≃+* S
g 
f: α → R
f 
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.88303
NonAssocSemiring 
R: Type ?u.88297
R] [
NonAssocSemiring: Type ?u.88306 → Type ?u.88306
NonAssocSemiring 
S: Type ?u.88300
S] (
g: R ≃+* S
g : 
R: Type ?u.88297
R ≃+* 
S: Type ?u.88300
S) (
f: α → R
f : 
α: Type ?u.88294
α → 
R: Type ?u.88297
R)
    (
s: Finset α
s : 
Finset: Type ?u.88685 → Type ?u.88685
Finset 
α: Type ?u.88294
α) : 
g: R ≃+* S
g (∑ 
x: ?m.95475
x in 
s: Finset α
s, 
f: α → R
f 
x: ?m.95475
x) = ∑ 
x: ?m.95695
x in 
s: Finset α
s, 
g: R ≃+* S
g (
f: α → R
f 
x: ?m.95695
x) :=
  
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 ≃+* S
g 
f: α → R
f 
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