Mathlib.Algebra.BigOperators.RingEquiv

RingEquiv.map_list_prod theorem

[Semiring R] [Semiring S] (f : R ≃+* S) (l : List R) : f l.prod = (l.map f).prod

Full source

protected theorem map_list_prod [Semiring R] [Semiring S] (f : R ≃+* S) (l : List R) :
    f l.prod = (l.map f).prod := map_list_prod f l

Ring Equivalence Preserves List Products

Informal description

Let $R$ and $S$ be semirings, and let $f : R \simeq+* S$ be a ring equivalence between them. For any list $l$ of elements in $R$, the image of the product of $l$ under $f$ is equal to the product of the list obtained by applying $f$ to each element of $l$. That is, $$ f\left(\prod_{x \in l} x\right) = \prod_{x \in l} f(x). $$

RingEquiv.map_list_sum theorem

[NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) (l : List R) : f l.sum = (l.map f).sum

Full source

protected theorem map_list_sum [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S]
    (f : R ≃+* S) (l : List R) : f l.sum = (l.map f).sum := map_list_sum f l

Ring Equivalence Preserves List Sums

Informal description

Let $R$ and $S$ be non-unital non-associative semirings, and let $f : R \simeq+* S$ be a ring equivalence between them. For any list $l$ of elements in $R$, the image of the sum of $l$ under $f$ is equal to the sum of the list obtained by applying $f$ to each element of $l$. That is, $$ f\left(\sum_{x \in l} x\right) = \sum_{x \in l} f(x). $$

RingEquiv.unop_map_list_prod theorem

 [Semiring R] [Semiring S] (f : R ≃+* Sᵐᵒᵖ) (l : List R) :
  MulOpposite.unop (f l.prod) = (l.map (MulOpposite.unop ∘ f)).reverse.prod

Full source

/-- An isomorphism into the opposite ring acts on the product by acting on the reversed elements -/
protected theorem unop_map_list_prod [Semiring R] [Semiring S] (f : R ≃+* Sᵐᵒᵖ) (l : List R) :
    MulOpposite.unop (f l.prod) = (l.map (MulOpposite.unopMulOpposite.unop ∘ f)).reverse.prod :=
  unop_map_list_prod f l

Ring Equivalence Maps List Product to Opposite Ring's Reversed Product

Informal description

Let $R$ and $S$ be semirings, and let $f : R \simeq+* S^\text{op}$ be a ring equivalence from $R$ to the opposite ring of $S$. For any list $l$ of elements in $R$, the unopposite of the image of the product of $l$ under $f$ is equal to the product of the reversed list obtained by applying the composition of the unopposite operation and $f$ to each element of $l$. That is, $$ \text{unop}\left(f\left(\prod_{x \in l} x\right)\right) = \prod_{x \in \text{reverse}(l)} \text{unop}(f(x)). $$

RingEquiv.map_multiset_prod theorem

[CommSemiring R] [CommSemiring S] (f : R ≃+* S) (s : Multiset R) : f s.prod = (s.map f).prod

Full source

protected theorem map_multiset_prod [CommSemiring R] [CommSemiring S] (f : R ≃+* S)
    (s : Multiset R) : f s.prod = (s.map f).prod :=
  map_multiset_prod f s

Ring Equivalence Preserves Multiset Products

Informal description

Let $R$ and $S$ be commutative semirings, and let $f : R \simeq+* S$ be a ring equivalence. For any multiset $s$ of elements in $R$, the image of the product of $s$ under $f$ is equal to the product of the multiset obtained by applying $f$ to each element of $s$. That is, $$ f\left(\prod_{x \in s} x\right) = \prod_{x \in s} f(x). $$

RingEquiv.map_multiset_sum theorem

[NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) (s : Multiset R) : f s.sum = (s.map f).sum

Full source

protected theorem map_multiset_sum [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S]
    (f : R ≃+* S) (s : Multiset R) : f s.sum = (s.map f).sum :=
  map_multiset_sum f s

Ring Equivalence Preserves Multiset Sums

Informal description

Let $R$ and $S$ be non-unital non-associative semirings, and let $f : R \simeq+* S$ be a ring equivalence. For any multiset $s$ of elements in $R$, the image of the sum of $s$ under $f$ is equal to the sum of the multiset obtained by applying $f$ to each element of $s$. That is, $$ f\left(\sum_{x \in s} x\right) = \sum_{x \in s} f(x). $$

RingEquiv.map_prod theorem

 [CommSemiring R] [CommSemiring S] (g : R ≃+* S) (f : α → R) (s : Finset α) : g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x)

Full source

protected theorem map_prod [CommSemiring R] [CommSemiring S] (g : R ≃+* S) (f : α → R)
    (s : Finset α) : g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x) :=
  map_prod g f s

Ring Equivalence Preserves Finite Products

Informal description

Let $R$ and $S$ be commutative semirings, and let $g : R \simeq+* S$ be a ring equivalence. For any function $f : \alpha \to R$ and any finite set $s \subseteq \alpha$, we have \[ g\left(\prod_{x \in s} f(x)\right) = \prod_{x \in s} g(f(x)). \]

RingEquiv.map_sum theorem

 [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (g : R ≃+* S) (f : α → R) (s : Finset α) :
  g (∑ x ∈ s, f x) = ∑ x ∈ s, g (f x)

Full source

protected theorem map_sum [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (g : R ≃+* S)
    (f : α → R) (s : Finset α) : g (∑ x ∈ s, f x) = ∑ x ∈ s, g (f x) :=
  map_sum g f s

Ring Equivalence Preserves Finite Sums

Informal description

Let $R$ and $S$ be non-unital non-associative semirings, and let $g : R \simeq+* S$ be a ring equivalence. For any function $f : \alpha \to R$ and any finite subset $s \subseteq \alpha$, we have \[ g\left(\sum_{x \in s} f(x)\right) = \sum_{x \in s} g(f(x)). \]