Results about mapping big operators across ring equivalences

ink

theorem RingEquiv.map_list_prod {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (f : R ≃+* S) (l : List R) : ↑f (List.prod l) = List.prod (List.map (↑f) l)

ink

theorem RingEquiv.map_list_sum {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R ≃+* S) (l : List R) : ↑f (List.sum l) = List.sum (List.map (↑f) l)

ink

theorem RingEquiv.unop_map_list_prod {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (f : R ≃+* Sᵐᵒᵖ) (l : List R) : (↑f (List.prod l)).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

ink

theorem RingEquiv.map_multiset_prod {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst : CommSemiring S] (f : R ≃+* S) (s : Multiset R) : ↑f (Multiset.prod s) = Multiset.prod (Multiset.map (↑f) s)

ink

theorem RingEquiv.map_multiset_sum {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R ≃+* S) (s : Multiset R) : ↑f (Multiset.sum s) = Multiset.sum (Multiset.map (↑f) s)

ink

theorem RingEquiv.map_prod {α : Type u_3} {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst : CommSemiring S] (g : R ≃+* S) (f : α → R) (s : Finset α) : ↑g (Finset.prod s fun x => f x) = Finset.prod s fun x => ↑g (f x)

ink

theorem RingEquiv.map_sum {α : Type u_3} {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (g : R ≃+* S) (f : α → R) (s : Finset α) : ↑g (Finset.sum s fun x => f x) = Finset.sum s fun x => ↑g (f x)