Pointwise big operators on finsets

This file contains basic results on applying big operators (product and sum) on finsets.

Implementation notes

We put all instances in the scope Pointwise, so that these instances are not available by default. Note that we do not mark them as reducible (as argued by note [reducible non-instances]) since we expect the scope to be open whenever the instances are actually used (and making the instances reducible changes the behavior of simp).

Tags

finset multiplication, finset addition, pointwise addition, pointwise multiplication, pointwise subtraction

@[simp]

theorem Finset.coe_prod {α : Type u_1} {ι : Type u_2} [CommMonoid α] [DecidableEq α] (s : Finset ι) (f : ι → Finset α) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)

@[simp]

theorem Finset.coe_sum {α : Type u_1} {ι : Type u_2} [AddCommMonoid α] [DecidableEq α] (s : Finset ι) (f : ι → Finset α) : ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

@[simp]

theorem Finset.prod_inv_index {α : Type u_1} {ι : Type u_2} [CommMonoid α] [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → α) : ∏ i ∈ s⁻¹, f i = ∏ i ∈ s, f i⁻¹

@[simp]

theorem Finset.sum_neg_index {α : Type u_1} {ι : Type u_2} [AddCommMonoid α] [DecidableEq ι] [InvolutiveNeg ι] (s : Finset ι) (f : ι → α) : ∑ i ∈ -s, f i = ∑ i ∈ s, f (-i)

@[simp]

theorem Finset.prod_neg_index {α : Type u_1} {ι : Type u_2} [CommMonoid α] [DecidableEq ι] [InvolutiveNeg ι] (s : Finset ι) (f : ι → α) : ∏ i ∈ -s, f i = ∏ i ∈ s, f (-i)

@[simp]

theorem Finset.sum_inv_index {α : Type u_1} {ι : Type u_2} [AddCommMonoid α] [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → α) : ∑ i ∈ s⁻¹, f i = ∑ i ∈ s, f i⁻¹