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_sum
{R : Type u_2}
{S : Type u_3}
[non_assoc_semiring R]
[non_assoc_semiring S]
(f : R ≃+* S)
(l : list R) :
@[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) :
mul_opposite.unop (⇑f l.prod) = (list.map (mul_opposite.unop ∘ ⇑f) l).reverse.prod
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}
[comm_semiring R]
[comm_semiring S]
(f : R ≃+* S)
(s : multiset R) :
@[protected]
theorem
ring_equiv.map_multiset_sum
{R : Type u_2}
{S : Type u_3}
[non_assoc_semiring R]
[non_assoc_semiring S]
(f : R ≃+* S)
(s : multiset R) :
@[protected]
theorem
ring_equiv.map_prod
{α : Type u_1}
{R : Type u_2}
{S : Type u_3}
[comm_semiring R]
[comm_semiring S]
(g : R ≃+* S)
(f : α → R)
(s : finset α) :
@[protected]
theorem
ring_equiv.map_sum
{α : Type u_1}
{R : Type u_2}
{S : Type u_3}
[non_assoc_semiring R]
[non_assoc_semiring S]
(g : R ≃+* S)
(f : α → R)
(s : finset α) :