Miscellaneous lemmas on big operators

The lemmas in this file have been moved out of Mathlib.Algebra.BigOperators.Group.Finset.Basic to reduce its imports.

theorem MonoidHom.coe_finset_prod {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MulOneClass β] [CommMonoid γ] (f : α → β →* γ) (s : Finset α) : ⇑(∏ x ∈ s, f x) = ∏ x ∈ s, ⇑(f x)

theorem AddMonoidHom.coe_finset_sum {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddZeroClass β] [AddCommMonoid γ] (f : α → β →+ γ) (s : Finset α) : ⇑(∑ x ∈ s, f x) = ∑ x ∈ s, ⇑(f x)

@[simp]

theorem MonoidHom.finset_prod_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MulOneClass β] [CommMonoid γ] (f : α → β →* γ) (s : Finset α) (b : β) : (∏ x ∈ s, f x) b = ∏ x ∈ s, (f x) b

See also Finset.prod_apply, with the same conclusion but with the weaker hypothesis f : α → β → γ

@[simp]

theorem AddMonoidHom.finset_sum_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddZeroClass β] [AddCommMonoid γ] (f : α → β →+ γ) (s : Finset α) (b : β) : (∑ x ∈ s, f x) b = ∑ x ∈ s, (f x) b

See also Finset.sum_apply, with the same conclusion but with the weaker hypothesis f : α → β → γ

theorem Finset.mulSupport_prod {ι : Type u_1} {α : Type u_2} {β : Type u_3} [CommMonoid β] (s : Finset ι) (f : ι → α → β) : (Function.mulSupport fun (x : α) => ∏ i ∈ s, f i x) ⊆ ⋃ i ∈ s, Function.mulSupport (f i)

theorem Finset.support_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommMonoid β] (s : Finset ι) (f : ι → α → β) : (Function.support fun (x : α) => ∑ i ∈ s, f i x) ⊆ ⋃ i ∈ s, Function.support (f i)

theorem Finset.isSquare_prod {ι : Type u_1} {α : Type u_2} {s : Finset ι} [CommMonoid α] (f : ι → α) (h : ∀ c ∈ s, IsSquare (f c)) : IsSquare (∏ i ∈ s, f i)

theorem Finset.even_sum {ι : Type u_1} {α : Type u_2} {s : Finset ι} [AddCommMonoid α] (f : ι → α) (h : ∀ c ∈ s, Even (f c)) : Even (∑ i ∈ s, f i)