Mathlib.Algebra.BigOperators.Group.Finset.Lemmas

MonoidHom.coe_finset_prod theorem

 [MulOneClass β] [CommMonoid γ] (f : α → β →* γ) (s : Finset α) : ⇑(∏ x ∈ s, f x) = ∏ x ∈ s, ⇑(f x)

Full source

@[to_additive]
theorem MonoidHom.coe_finset_prod [MulOneClass β] [CommMonoid γ] (f : α → β →* γ) (s : Finset α) :
    ⇑(∏ x ∈ s, f x) = ∏ x ∈ s, ⇑(f x) :=
  map_prod (MonoidHom.coeFn β γ) _ _

Product of Monoid Homomorphisms Equals Pointwise Product of Functions

Informal description

Let $\beta$ be a monoid and $\gamma$ a commutative monoid. For any family of monoid homomorphisms $f : \alpha \to (\beta \to^* \gamma)$ and any finite set $s \subseteq \alpha$, the underlying function of the product $\prod_{x \in s} f(x)$ is equal to the pointwise product of the underlying functions $\prod_{x \in s} f(x)(-)$.

MonoidHom.finset_prod_apply theorem

 [MulOneClass β] [CommMonoid γ] (f : α → β →* γ) (s : Finset α) (b : β) : (∏ x ∈ s, f x) b = ∏ x ∈ s, f x b

Full source

/-- See also `Finset.prod_apply`, with the same conclusion but with the weaker hypothesis
`f : α → β → γ` -/
@[to_additive (attr := simp)
  "See also `Finset.sum_apply`, with the same conclusion but with the weaker hypothesis
  `f : α → β → γ`"]
theorem MonoidHom.finset_prod_apply [MulOneClass β] [CommMonoid γ] (f : α → β →* γ) (s : Finset α)
    (b : β) : (∏ x ∈ s, f x) b = ∏ x ∈ s, f x b :=
  map_prod (MonoidHom.eval b) _ _

Evaluation of Product Homomorphism Equals Product of Evaluations

Informal description

Let $\beta$ be a monoid and $\gamma$ a commutative monoid. For any family of monoid homomorphisms $f : \alpha \to (\beta \to \gamma)$, any finite set $s \subseteq \alpha$, and any element $b \in \beta$, the evaluation of the product homomorphism $\prod_{x \in s} f(x)$ at $b$ is equal to the product $\prod_{x \in s} f(x)(b)$ in $\gamma$.

Finset.mulSupport_prod theorem

(s : Finset ι) (f : ι → α → β) : mulSupport (fun x ↦ ∏ i ∈ s, f i x) ⊆ ⋃ i ∈ s, mulSupport (f i)

Full source

@[to_additive]
lemma mulSupport_prod (s : Finset ι) (f : ι → α → β) :
    mulSupportmulSupport (fun x ↦ ∏ i ∈ s, f i x) ⊆ ⋃ i ∈ s, mulSupport (f i) := by
  simp only [mulSupport_subset_iff', Set.mem_iUnion, not_exists, nmem_mulSupport]
  exact fun x ↦ prod_eq_one

Multiplicative Support of a Product is Contained in the Union of Supports

Informal description

Let $s$ be a finite set of indices and $f : \iota \to \alpha \to \beta$ a family of functions into a commutative monoid $\beta$. The multiplicative support of the product function $\prod_{i \in s} f(i)(x)$ is contained in the union of the multiplicative supports of the individual functions $f(i)$, i.e., \[ \{x \mid \prod_{i \in s} f(i)(x) \neq 1\} \subseteq \bigcup_{i \in s} \{x \mid f(i)(x) \neq 1\}. \]

Finset.isSquare_prod theorem

{s : Finset ι} [CommMonoid α] (f : ι → α) (h : ∀ c ∈ s, IsSquare (f c)) : IsSquare (∏ i ∈ s, f i)

Full source

@[to_additive]
lemma isSquare_prod {s : Finset ι} [CommMonoid α] (f : ι → α)
    (h : ∀ c ∈ s, IsSquare (f c)) : IsSquare (∏ i ∈ s, f i) := by
  rw [isSquare_iff_exists_sq]
  use (∏ (x : s), ((isSquare_iff_exists_sq _).mp (h _ x.2)).choose)
  rw [@sq, ← Finset.prod_mul_distrib, ← Finset.prod_coe_sort]
  congr
  ext i
  rw [← @sq]
  exact ((isSquare_iff_exists_sq _).mp (h _ i.2)).choose_spec

Product of Squares is Square in a Commutative Monoid

Informal description

Let $\alpha$ be a commutative monoid, $s$ a finite set, and $f : \iota \to \alpha$ a function. If for every $c \in s$, the element $f(c)$ is a square in $\alpha$, then the product $\prod_{i \in s} f(i)$ is also a square in $\alpha$.