Mathlib.Algebra.BigOperators.GroupWithZero.Action

List.smul_sum theorem

{r : α} {l : List β} : r • l.sum = (l.map (r • ·)).sum

Full source

theorem List.smul_sum {r : α} {l : List β} : r • l.sum = (l.map (r • ·)).sum :=
  map_list_sum (DistribSMul.toAddMonoidHom β r) l

Scalar Multiplication Distributes over List Summation

Informal description

For any scalar $r$ in a type $\alpha$ and any list $l$ of elements in a type $\beta$ equipped with an additive monoid structure, the scalar multiplication of $r$ with the sum of $l$ is equal to the sum of the list obtained by applying $r \cdot$ to each element of $l$. In symbols: $$ r \cdot \sum_{x \in l} x = \sum_{x \in l} (r \cdot x). $$

List.smul_prod' theorem

{r : α} {l : List β} : r • l.prod = (l.map (r • ·)).prod

Full source

theorem List.smul_prod' {r : α} {l : List β} : r • l.prod = (l.map (r • ·)).prod :=
  map_list_prod (MulDistribMulAction.toMonoidHom β r) l

Distributive Action Preserves List Products: $r \cdot \prod x = \prod (r \cdot x)$

Informal description

Let $r$ be an element of a monoid $\alpha$ acting distributively on another monoid $\beta$, and let $l$ be a list of elements in $\beta$. Then the scalar multiplication of $r$ with the product of the list $l$ is equal to the product of the list obtained by applying the scalar multiplication $r \cdot (\cdot)$ to each element of $l$. That is, \[ r \cdot \left( \prod_{x \in l} x \right) = \prod_{x \in l} (r \cdot x). \]

Multiset.smul_sum theorem

{s : Multiset β} : r • s.sum = (s.map (r • ·)).sum

Full source

theorem Multiset.smul_sum {s : Multiset β} : r • s.sum = (s.map (r • ·)).sum :=
  (DistribSMul.toAddMonoidHom β r).map_multiset_sum s

Scalar Multiplication Distributes over Multiset Summation

Informal description

For any scalar $r$ and any multiset $s$ of elements in an additive commutative monoid $\beta$, the scalar multiplication of $r$ with the sum of $s$ is equal to the sum of the multiset obtained by applying $r \cdot (\cdot)$ to each element of $s$. That is, \[ r \cdot \left( \sum_{x \in s} x \right) = \sum_{x \in s} (r \cdot x). \]

Finset.smul_sum theorem

{f : γ → β} {s : Finset γ} : (r • ∑ x ∈ s, f x) = ∑ x ∈ s, r • f x

Full source

theorem Finset.smul_sum {f : γ → β} {s : Finset γ} :
    (r • ∑ x ∈ s, f x) = ∑ x ∈ s, r • f x :=
  map_sum (DistribSMul.toAddMonoidHom β r) f s

Scalar Multiplication Distributes over Finite Sum

Informal description

Let $r$ be a scalar, $s$ be a finite set, and $f : \gamma \to \beta$ be a function. Then the scalar multiplication of $r$ with the sum of $f$ over $s$ equals the sum of $r \cdot f(x)$ over all $x \in s$, i.e., $$ r \cdot \left( \sum_{x \in s} f(x) \right) = \sum_{x \in s} (r \cdot f(x)). $$

smul_finsum_mem theorem

{f : γ → β} {s : Set γ} (hs : s.Finite) : r • ∑ᶠ x ∈ s, f x = ∑ᶠ x ∈ s, r • f x

Full source

theorem smul_finsum_mem {f : γ → β} {s : Set γ} (hs : s.Finite) :
    r • ∑ᶠ x ∈ s, f x = ∑ᶠ x ∈ s, r • f x :=
  (DistribSMul.toAddMonoidHom β r).map_finsum_mem f hs

Scalar Multiplication Distributes over Finite Summation on a Finite Set

Informal description

Let $r$ be a scalar, $f : \gamma \to \beta$ be a function, and $s$ be a finite subset of $\gamma$. Then the scalar multiplication of $r$ with the finite sum of $f$ over $s$ equals the finite sum of $r \cdot f(x)$ over all $x \in s$, i.e., \[ r \cdot \left( \sum_{x \in s} f(x) \right) = \sum_{x \in s} (r \cdot f(x)). \]

Multiset.smul_prod' theorem

{r : α} {s : Multiset β} : r • s.prod = (s.map (r • ·)).prod

Full source

theorem Multiset.smul_prod' {r : α} {s : Multiset β} : r • s.prod = (s.map (r • ·)).prod :=
  (MulDistribMulAction.toMonoidHom β r).map_multiset_prod s

Distributive Action Commutes with Multiset Product: $r \cdot \prod_{x \in s} x = \prod_{x \in s} (r \cdot x)$

Informal description

Let $\alpha$ and $\beta$ be monoids where $\alpha$ acts distributively on $\beta$ via multiplication. For any element $r \in \alpha$ and any multiset $s$ over $\beta$, the scalar multiplication of $r$ with the product of $s$ equals the product of the multiset obtained by applying $r \cdot$ to each element of $s$. That is, \[ r \cdot \left( \prod_{x \in s} x \right) = \prod_{x \in s} (r \cdot x). \]

Finset.smul_prod' theorem

{r : α} {f : γ → β} {s : Finset γ} : (r • ∏ x ∈ s, f x) = ∏ x ∈ s, r • f x

Full source

theorem Finset.smul_prod' {r : α} {f : γ → β} {s : Finset γ} :
    (r • ∏ x ∈ s, f x) = ∏ x ∈ s, r • f x :=
  map_prod (MulDistribMulAction.toMonoidHom β r) f s

Distributive Action Commutes with Finite Product: $r \cdot \prod_{x \in s} f(x) = \prod_{x \in s} r \cdot f(x)$

Informal description

Let $\alpha$ and $\beta$ be monoids where $\alpha$ acts distributively on $\beta$ via multiplication. For any element $r \in \alpha$, any function $f : \gamma \to \beta$, and any finite set $s \subseteq \gamma$, we have \[ r \cdot \left( \prod_{x \in s} f(x) \right) = \prod_{x \in s} (r \cdot f(x)). \]

smul_finprod' theorem

{ι : Sort*} [Finite ι] {f : ι → β} (r : α) : r • ∏ᶠ x : ι, f x = ∏ᶠ x : ι, r • (f x)

Full source

theorem smul_finprod' {ι : Sort*} [Finite ι] {f : ι → β} (r : α) :
    r • ∏ᶠ x : ι, f x = ∏ᶠ x : ι, r • (f x) := by
  cases nonempty_fintype (PLift ι)
  simp only [finprod_eq_prod_plift_of_mulSupport_subset (s := Finset.univ) (by simp),
    finprod_eq_prod_of_fintype, Finset.smul_prod']

Distributive Action Commutes with Finite Product over Finite Types: $r \cdot \prod_{x} f(x) = \prod_{x} r \cdot f(x)$

Informal description

Let $\alpha$ and $\beta$ be monoids where $\alpha$ acts distributively on $\beta$ via multiplication. For any finite type $\iota$, any function $f : \iota \to \beta$, and any element $r \in \alpha$, we have \[ r \cdot \left( \prod_{x \in \iota} f(x) \right) = \prod_{x \in \iota} (r \cdot f(x)), \] where the product is taken over all elements of $\iota$.

Finset.smul_prod_perm theorem

[Fintype G] (b : β) (g : G) : (g • ∏ h : G, h • b) = ∏ h : G, h • b

Full source

theorem Finset.smul_prod_perm [Fintype G] (b : β) (g : G) :
    (g • ∏ h : G, h • b) = ∏ h : G, h • b := by
  simp only [smul_prod', smul_smul]
  exact Finset.prod_bijective (g * ·) (Group.mulLeft_bijective g) (by simp) (fun _ _ ↦ rfl)

Invariance of Group Action on Product: $g \cdot \prod_{h \in G} (h \cdot b) = \prod_{h \in G} (h \cdot b)$

Informal description

Let $G$ be a finite group acting on a monoid $\beta$ via a multiplicative distributive action. For any element $b \in \beta$ and any group element $g \in G$, the action of $g$ on the product $\prod_{h \in G} (h \cdot b)$ equals the product $\prod_{h \in G} (h \cdot b)$, i.e., \[ g \cdot \left( \prod_{h \in G} (h \cdot b) \right) = \prod_{h \in G} (h \cdot b). \]

smul_finprod_perm theorem

[Finite G] (b : β) (g : G) : (g • ∏ᶠ h : G, h • b) = ∏ᶠ h : G, h • b

Full source

theorem smul_finprod_perm [Finite G] (b : β) (g : G) :
    (g • ∏ᶠ h : G, h • b) = ∏ᶠ h : G, h • b := by
  cases nonempty_fintype G
  simp only [finprod_eq_prod_of_fintype, Finset.smul_prod_perm]

Invariance of Finite Product under Group Action: $g \cdot \prod_{h \in G} (h \cdot b) = \prod_{h \in G} (h \cdot b)$

Informal description

Let $G$ be a finite group acting on a commutative monoid $\beta$ via a multiplicative distributive action. For any element $b \in \beta$ and any group element $g \in G$, the action of $g$ on the finite product $\prod_{h \in G} (h \cdot b)$ equals the finite product $\prod_{h \in G} (h \cdot b)$, i.e., \[ g \cdot \left( \prod_{h \in G} (h \cdot b) \right) = \prod_{h \in G} (h \cdot b). \]

List.smul_prod theorem

 [Monoid α] [MulOneClass β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] (l : List β) (m : α) :
  m ^ l.length • l.prod = (l.map (m • ·)).prod

Full source

@[to_additive]
theorem smul_prod [Monoid α] [MulOneClass β] [MulAction α β] [IsScalarTower α β β]
    [SMulCommClass α β β] (l : List β) (m : α) :
    m ^ l.length • l.prod = (l.map (m • ·)).prod := by
  induction l with
  | nil => simp
  | cons head tail ih => simp [← ih, smul_mul_smul_comm, pow_succ']

Scalar Multiplication Commutes with List Product: $m^{|l|} \cdot \prod l = \prod (m \cdot x)$ for $x \in l$

Informal description

Let $\alpha$ be a monoid and $\beta$ a multiplicative monoid with identity, equipped with a multiplicative action of $\alpha$ on $\beta$. Suppose that: 1. The scalar multiplication satisfies the tower property `IsScalarTower α β β`, 2. The scalar multiplication of $\alpha$ on $\beta$ commutes with itself (`SMulCommClass α β β`). Then for any list $l$ of elements in $\beta$ and any element $m \in \alpha$, we have: $$m^{|l|} \cdot \prod_{x \in l} x = \prod_{x \in l} (m \cdot x),$$ where $|l|$ denotes the length of the list $l$, $\prod$ denotes the product of elements in the list, and $\cdot$ denotes the scalar multiplication of $\alpha$ on $\beta$.

Multiset.smul_prod theorem

 [Monoid α] [CommMonoid β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] (s : Multiset β) (b : α) :
  b ^ card s • s.prod = (s.map (b • ·)).prod

Full source

@[to_additive]
theorem smul_prod [Monoid α] [CommMonoid β] [MulAction α β] [IsScalarTower α β β]
    [SMulCommClass α β β] (s : Multiset β) (b : α) :
    b ^ card s • s.prod = (s.map (b • ·)).prod :=
  Quot.induction_on s <| by simp [List.smul_prod]

Scalar Multiplication Commutes with Multiset Product: $b^{|s|} \cdot \prod s = \prod (b \cdot x)$ for $x \in s$

Informal description

Let $\alpha$ be a monoid and $\beta$ a commutative monoid, with $\alpha$ acting multiplicatively on $\beta$ such that: 1. The scalar multiplication satisfies the tower property (i.e., for $a \in \alpha$, $x, y \in \beta$, $(a \cdot x) \cdot y = a \cdot (x \cdot y)$), 2. The scalar multiplication of $\alpha$ on $\beta$ commutes with itself (i.e., for $a, a' \in \alpha$, $x \in \beta$, $a \cdot (a' \cdot x) = a' \cdot (a \cdot x)$). Then for any multiset $s$ of elements in $\beta$ and any element $b \in \alpha$, we have: $$ b^{|s|} \cdot \prod_{x \in s} x = \prod_{x \in s} (b \cdot x), $$ where $|s|$ denotes the cardinality of $s$, $\cdot$ denotes the scalar multiplication, and $\prod$ denotes the product in $\beta$.

Finset.smul_prod theorem

 [CommMonoid β] [Monoid α] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] (s : Finset β) (b : α)
  (f : β → β) : b ^ s.card • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x

Full source

theorem smul_prod
    [CommMonoid β] [Monoid α] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β]
    (s : Finset β) (b : α) (f : β → β) :
    b ^ s.card • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x := by
  have : Multiset.map (fun (x : β) ↦ b • f x) s.val =
      Multiset.map (fun x ↦ b • x) (Multiset.map f s.val) := by
    simp only [Multiset.map_map, Function.comp_apply]
  simp_rw [prod_eq_multiset_prod, card_def, this, ← Multiset.smul_prod _ b, Multiset.card_map]

Scalar Multiplication Commutes with Finite Product: $b^{\#s} \cdot \prod f = \prod (b \cdot f)$

Informal description

Let $\alpha$ be a monoid and $\beta$ a commutative monoid, with $\alpha$ acting multiplicatively on $\beta$ such that: 1. The scalar multiplication satisfies the tower property (i.e., for $a \in \alpha$, $b, c \in \beta$, $(a \cdot b) \cdot c = a \cdot (b \cdot c)$), 2. The scalar multiplication of $\alpha$ on $\beta$ commutes with itself (i.e., for $a, a' \in \alpha$, $b \in \beta$, $a \cdot (a' \cdot b) = a' \cdot (a \cdot b)$). Then for any finite subset $s$ of $\beta$, any element $b \in \alpha$, and any function $f : \beta \to \beta$, we have: $$ b^{\#s} \cdot \prod_{x \in s} f(x) = \prod_{x \in s} (b \cdot f(x)), $$ where $\#s$ denotes the cardinality of $s$, $\cdot$ denotes the scalar multiplication of $\alpha$ on $\beta$, and $\prod$ denotes the product in the commutative monoid $\beta$.

Finset.prod_smul theorem

 [CommMonoid β] [CommMonoid α] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] (s : Finset β) (b : β → α)
  (f : β → β) : ∏ i ∈ s, b i • f i = (∏ i ∈ s, b i) • ∏ i ∈ s, f i

Full source

theorem prod_smul
    [CommMonoid β] [CommMonoid α] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β]
    (s : Finset β) (b : β → α) (f : β → β) :
    ∏ i ∈ s, b i • f i = (∏ i ∈ s, b i) • ∏ i ∈ s, f i := by
  induction s using Finset.cons_induction_on with
  | empty =>  simp
  | cons _ _ hj ih => rw [prod_cons, ih, smul_mul_smul_comm, ← prod_cons hj, ← prod_cons hj]

Product of Scalar Multiples Equals Scalar Multiple of Products in Commutative Monoids

Informal description

Let $\alpha$ and $\beta$ be commutative monoids, with $\alpha$ acting multiplicatively on $\beta$ such that: 1. The scalar multiplication satisfies the tower property (`IsScalarTower α β β`), 2. The scalar multiplication of $\alpha$ on $\beta$ commutes with itself (`SMulCommClass α β β`). Then for any finite subset $s$ of $\beta$, any function $b : \beta \to \alpha$, and any function $f : \beta \to \beta$, we have: $$ \prod_{i \in s} (b(i) \cdot f(i)) = \left(\prod_{i \in s} b(i)\right) \cdot \left(\prod_{i \in s} f(i)\right), $$ where $\cdot$ denotes the scalar multiplication of $\alpha$ on $\beta$ and the products are taken in their respective monoids.