Results about mapping big operators across ring equivalences #
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)
:
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)
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)
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)
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)