Miscellaneous lemmas on big operators

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

theorem MonoidHom.coe_finsetProd {ι : Type u_1} {M : Type u_3} {N : Type u_4} [MulOneClass M] [CommMonoid N] (f : ι → M →* N) (s : Finset ι) : ⇑(∏ x ∈ s, f x) = ∏ x ∈ s, ⇑(f x)

theorem AddMonoidHom.coe_finsetSum {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddCommMonoid N] (f : ι → M →+ N) (s : Finset ι) : ⇑(∑ x ∈ s, f x) = ∑ x ∈ s, ⇑(f x)

@[simp]

theorem MonoidHom.finsetProd_apply {ι : Type u_1} {M : Type u_3} {N : Type u_4} [MulOneClass M] [CommMonoid N] (f : ι → M →* N) (s : Finset ι) (b : M) : (∏ 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 : α → M → N

@[simp]

theorem AddMonoidHom.finsetSum_apply {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddCommMonoid N] (f : ι → M →+ N) (s : Finset ι) (b : M) : (∑ 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 : α → M → N

theorem Finset.mulSupport_prod {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [CommMonoid M] (s : Finset ι) (f : ι → κ → M) : (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} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → κ → M) : (Function.support fun (x : κ) => ∑ i ∈ s, f i x) ⊆ ⋃ i ∈ s, Function.support (f i)

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

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