Finite products and sums over types and sets

We define products and sums over types and subsets of types, with no finiteness hypotheses. All infinite products and sums are defined to be junk values (i.e. one or zero). This approach is sometimes easier to use than Finset.sum, when issues arise with Finset and Fintype being data.

Main definitions

We use the following variables:

• α, β - types with no structure;
• s, t - sets
• M, N - additive or multiplicative commutative monoids
• f, g - functions

Definitions in this file:

• finsum f : M : the sum of f x as x ranges over the support of f, if it's finite. Zero otherwise.

• finprod f : M : the product of f x as x ranges over the multiplicative support of f, if it's finite. One otherwise.

Notation

• ∑ᶠ i, f i and ∑ᶠ i : α, f i for finsum f

• ∏ᶠ i, f i and ∏ᶠ i : α, f i for finprod f

This notation works for functions f : p → M, where p : Prop, so the following works:

• ∑ᶠ i ∈ s, f i, where f : α → M, s : Set α : sum over the set s;
• ∑ᶠ n < 5, f n, where f : ℕ → M : same as f 0 + f 1 + f 2 + f 3 + f 4;
• ∏ᶠ (n >= -2) (hn : n < 3), f n, where f : ℤ → M : same as f (-2) * f (-1) * f 0 * f 1 * f 2.

Implementation notes

finsum and finprod is "yet another way of doing finite sums and products in Lean". However experiments in the wild (e.g. with matroids) indicate that it is a helpful approach in settings where the user is not interested in computability and wants to do reasoning without running into typeclass diamonds caused by the constructive finiteness used in definitions such as Finset and Fintype. By sticking solely to Set.Finite we avoid these problems. We are aware that there are other solutions but for beginner mathematicians this approach is easier in practice.

Another application is the construction of a partition of unity from a collection of “bump” function. In this case the finite set depends on the point and it's convenient to have a definition that does not mention the set explicitly.

The first arguments in all definitions and lemmas is the codomain of the function of the big operator. This is necessary for the heuristic in @[to_additive]. See the documentation of to_additive.attr for more information.

We did not add IsFinite (X : Type) : Prop, because it is simply Nonempty (Fintype X).

Tags

finsum, finprod, finite sum, finite product

Definition and relation to Finset.sum and Finset.prod

theorem finsum_def' {M : Type u_7} {α : Sort u_8} [AddCommMonoid M] (f : α → M) : finsum f = if h : Set.Finite (Function.support (f ∘ PLift.down)) then Finset.sum (Set.Finite.toFinset h) fun (i : PLift α) => f i.down else 0

@[irreducible]

noncomputable def finsum {M : Type u_7} {α : Sort u_8} [AddCommMonoid M] (f : α → M) : M

Sum of f x as x ranges over the elements of the support of f, if it's finite. Zero otherwise.

Equations

• @finsum = wrapped✝.1

theorem finprod_def' {M : Type u_7} {α : Sort u_8} [CommMonoid M] (f : α → M) : finprod f = if h : Set.Finite (Function.mulSupport (f ∘ PLift.down)) then Finset.prod (Set.Finite.toFinset h) fun (i : PLift α) => f i.down else 1

@[irreducible]

noncomputable def finprod {M : Type u_7} {α : Sort u_8} [CommMonoid M] (f : α → M) : M

Product of f x as x ranges over the elements of the multiplicative support of f, if it's finite. One otherwise.

Equations

• @finprod = wrapped✝.1

def BigOperators.«term∑ᶠ_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def BigOperators.«term∑ᶠ_,_» : Lean.ParserDescr

∑ᶠ x, f x is notation for finsum f. It is the sum of f x, where x ranges over the support of f, if it's finite, zero otherwise. Taking the sum over multiple arguments or conditions is possible, e.g. ∏ᶠ (x) (y), f x y and ∏ᶠ (x) (h: x ∈ s), f x

Equations

• One or more equations did not get rendered due to their size.

def BigOperators.«term∏ᶠ_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def BigOperators.«term∏ᶠ_,_» : Lean.ParserDescr

∏ᶠ x, f x is notation for finprod f. It is the sum of f x, where x ranges over the multiplicative support of f, if it's finite, one otherwise. Taking the product over multiple arguments or conditions is possible, e.g. ∏ᶠ (x) (y), f x y and ∏ᶠ (x) (h: x ∈ s), f x

Equations

• One or more equations did not get rendered due to their size.

theorem finsum_eq_sum_plift_of_support_toFinset_subset {M : Type u_2} {α : Sort u_4} [AddCommMonoid M] {f : α → M} (hf : Set.Finite (Function.support (f ∘ PLift.down))) {s : Finset (PLift α)} (hs : Set.Finite.toFinset hf ⊆ s) : (finsum fun (i : α) => f i) = Finset.sum s fun (i : PLift α) => f i.down

theorem finprod_eq_prod_plift_of_mulSupport_toFinset_subset {M : Type u_2} {α : Sort u_4} [CommMonoid M] {f : α → M} (hf : Set.Finite (Function.mulSupport (f ∘ PLift.down))) {s : Finset (PLift α)} (hs : Set.Finite.toFinset hf ⊆ s) : (finprod fun (i : α) => f i) = Finset.prod s fun (i : PLift α) => f i.down

theorem finsum_eq_sum_plift_of_support_subset {M : Type u_2} {α : Sort u_4} [AddCommMonoid M] {f : α → M} {s : Finset (PLift α)} (hs : Function.support (f ∘ PLift.down) ⊆ ↑s) : (finsum fun (i : α) => f i) = Finset.sum s fun (i : PLift α) => f i.down

theorem finprod_eq_prod_plift_of_mulSupport_subset {M : Type u_2} {α : Sort u_4} [CommMonoid M] {f : α → M} {s : Finset (PLift α)} (hs : Function.mulSupport (f ∘ PLift.down) ⊆ ↑s) : (finprod fun (i : α) => f i) = Finset.prod s fun (i : PLift α) => f i.down

@[simp]

theorem finsum_zero {M : Type u_2} {α : Sort u_4} [AddCommMonoid M] : (finsum fun (x : α) => 0) = 0

@[simp]

theorem finprod_one {M : Type u_2} {α : Sort u_4} [CommMonoid M] : (finprod fun (x : α) => 1) = 1

theorem finsum_of_isEmpty {M : Type u_2} {α : Sort u_4} [AddCommMonoid M] [IsEmpty α] (f : α → M) : (finsum fun (i : α) => f i) = 0

theorem finprod_of_isEmpty {M : Type u_2} {α : Sort u_4} [CommMonoid M] [IsEmpty α] (f : α → M) : (finprod fun (i : α) => f i) = 1

@[simp]

theorem finsum_false {M : Type u_2} [AddCommMonoid M] (f : False → M) : (finsum fun (i : False) => f i) = 0

@[simp]

theorem finprod_false {M : Type u_2} [CommMonoid M] (f : False → M) : (finprod fun (i : False) => f i) = 1

theorem finsum_eq_single {M : Type u_2} {α : Sort u_4} [AddCommMonoid M] (f : α → M) (a : α) (ha : ∀ (x : α), x ≠ a → f x = 0) : (finsum fun (x : α) => f x) = f a

theorem finprod_eq_single {M : Type u_2} {α : Sort u_4} [CommMonoid M] (f : α → M) (a : α) (ha : ∀ (x : α), x ≠ a → f x = 1) : (finprod fun (x : α) => f x) = f a

theorem finsum_unique {M : Type u_2} {α : Sort u_4} [AddCommMonoid M] [Unique α] (f : α → M) : (finsum fun (i : α) => f i) = f default

theorem finprod_unique {M : Type u_2} {α : Sort u_4} [CommMonoid M] [Unique α] (f : α → M) : (finprod fun (i : α) => f i) = f default

@[simp]

theorem finsum_true {M : Type u_2} [AddCommMonoid M] (f : True → M) : (finsum fun (i : True) => f i) = f trivial

@[simp]

theorem finprod_true {M : Type u_2} [CommMonoid M] (f : True → M) : (finprod fun (i : True) => f i) = f trivial

theorem finsum_eq_dif {M : Type u_2} [AddCommMonoid M] {p : Prop} [Decidable p] (f : p → M) : (finsum fun (i : p) => f i) = if h : p then f h else 0

theorem finprod_eq_dif {M : Type u_2} [CommMonoid M] {p : Prop} [Decidable p] (f : p → M) : (finprod fun (i : p) => f i) = if h : p then f h else 1

theorem finsum_eq_if {M : Type u_2} [AddCommMonoid M] {p : Prop} [Decidable p] {x : M} : (finsum fun (x_1 : p) => x) = if p then x else 0

theorem finprod_eq_if {M : Type u_2} [CommMonoid M] {p : Prop} [Decidable p] {x : M} : (finprod fun (x_1 : p) => x) = if p then x else 1

theorem finsum_congr {M : Type u_2} {α : Sort u_4} [AddCommMonoid M] {f : α → M} {g : α → M} (h : ∀ (x : α), f x = g x) : finsum f = finsum g

theorem finprod_congr {M : Type u_2} {α : Sort u_4} [CommMonoid M] {f : α → M} {g : α → M} (h : ∀ (x : α), f x = g x) : finprod f = finprod g

theorem finsum_congr_Prop {M : Type u_2} [AddCommMonoid M] {p : Prop} {q : Prop} {f : p → M} {g : q → M} (hpq : p = q) (hfg : ∀ (h : q), f ⋯ = g h) : finsum f = finsum g

theorem finprod_congr_Prop {M : Type u_2} [CommMonoid M] {p : Prop} {q : Prop} {f : p → M} {g : q → M} (hpq : p = q) (hfg : ∀ (h : q), f ⋯ = g h) : finprod f = finprod g

theorem finsum_induction {M : Type u_2} {α : Sort u_4} [AddCommMonoid M] {f : α → M} (p : M → Prop) (hp₀ : p 0) (hp₁ : ∀ (x y : M), p x → p y → p (x + y)) (hp₂ : ∀ (i : α), p (f i)) : p (finsum fun (i : α) => f i)

To prove a property of a finite sum, it suffices to prove that the property is additive and holds on the summands.

theorem finprod_induction {M : Type u_2} {α : Sort u_4} [CommMonoid M] {f : α → M} (p : M → Prop) (hp₀ : p 1) (hp₁ : ∀ (x y : M), p x → p y → p (x * y)) (hp₂ : ∀ (i : α), p (f i)) : p (finprod fun (i : α) => f i)

To prove a property of a finite product, it suffices to prove that the property is multiplicative and holds on the factors.

theorem finprod_nonneg {α : Sort u_4} {R : Type u_7} [OrderedCommSemiring R] {f : α → R} (hf : ∀ (x : α), 0 ≤ f x) : 0 ≤ finprod fun (x : α) => f x

theorem finsum_nonneg {α : Sort u_4} {M : Type u_7} [OrderedAddCommMonoid M] {f : α → M} (hf : ∀ (i : α), 0 ≤ f i) : 0 ≤ finsum fun (i : α) => f i

theorem one_le_finprod' {α : Sort u_4} {M : Type u_7} [OrderedCommMonoid M] {f : α → M} (hf : ∀ (i : α), 1 ≤ f i) : 1 ≤ finprod fun (i : α) => f i

theorem AddMonoidHom.map_finsum_plift {M : Type u_2} {N : Type u_3} {α : Sort u_4} [AddCommMonoid M] [AddCommMonoid N] (f : M →+ N) (g : α → M) (h : Set.Finite (Function.support (g ∘ PLift.down))) : f (finsum fun (x : α) => g x) = finsum fun (x : α) => f (g x)

theorem MonoidHom.map_finprod_plift {M : Type u_2} {N : Type u_3} {α : Sort u_4} [CommMonoid M] [CommMonoid N] (f : M →* N) (g : α → M) (h : Set.Finite (Function.mulSupport (g ∘ PLift.down))) : f (finprod fun (x : α) => g x) = finprod fun (x : α) => f (g x)

theorem AddMonoidHom.map_finsum_Prop {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] {p : Prop} (f : M →+ N) (g : p → M) : f (finsum fun (x : p) => g x) = finsum fun (x : p) => f (g x)

theorem MonoidHom.map_finprod_Prop {M : Type u_2} {N : Type u_3} [CommMonoid M] [CommMonoid N] {p : Prop} (f : M →* N) (g : p → M) : f (finprod fun (x : p) => g x) = finprod fun (x : p) => f (g x)

theorem AddMonoidHom.map_finsum_of_preimage_zero {M : Type u_2} {N : Type u_3} {α : Sort u_4} [AddCommMonoid M] [AddCommMonoid N] (f : M →+ N) (hf : ∀ (x : M), f x = 0 → x = 0) (g : α → M) : f (finsum fun (i : α) => g i) = finsum fun (i : α) => f (g i)

theorem MonoidHom.map_finprod_of_preimage_one {M : Type u_2} {N : Type u_3} {α : Sort u_4} [CommMonoid M] [CommMonoid N] (f : M →* N) (hf : ∀ (x : M), f x = 1 → x = 1) (g : α → M) : f (finprod fun (i : α) => g i) = finprod fun (i : α) => f (g i)

theorem AddMonoidHom.map_finsum_of_injective {M : Type u_2} {N : Type u_3} {α : Sort u_4} [AddCommMonoid M] [AddCommMonoid N] (g : M →+ N) (hg : Function.Injective ⇑g) (f : α → M) : g (finsum fun (i : α) => f i) = finsum fun (i : α) => g (f i)

theorem MonoidHom.map_finprod_of_injective {M : Type u_2} {N : Type u_3} {α : Sort u_4} [CommMonoid M] [CommMonoid N] (g : M →* N) (hg : Function.Injective ⇑g) (f : α → M) : g (finprod fun (i : α) => f i) = finprod fun (i : α) => g (f i)

theorem AddEquiv.map_finsum {M : Type u_2} {N : Type u_3} {α : Sort u_4} [AddCommMonoid M] [AddCommMonoid N] (g : M ≃+ N) (f : α → M) : g (finsum fun (i : α) => f i) = finsum fun (i : α) => g (f i)

theorem MulEquiv.map_finprod {M : Type u_2} {N : Type u_3} {α : Sort u_4} [CommMonoid M] [CommMonoid N] (g : M ≃* N) (f : α → M) : g (finprod fun (i : α) => f i) = finprod fun (i : α) => g (f i)

theorem finsum_smul {ι : Sort u_6} {R : Type u_7} {M : Type u_8} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : ι → R) (x : M) : (finsum fun (i : ι) => f i) • x = finsum fun (i : ι) => f i • x

The NoZeroSMulDivisors makes sure that the result holds even when the support of f is infinite. For a more usual version assuming (support f).Finite instead, see finsum_smul'.

theorem smul_finsum {ι : Sort u_6} {R : Type u_7} {M : Type u_8} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (c : R) (f : ι → M) : (c • finsum fun (i : ι) => f i) = finsum fun (i : ι) => c • f i

The NoZeroSMulDivisors makes sure that the result holds even when the support of f is infinite. For a more usual version assuming (support f).Finite instead, see smul_finsum'.

theorem finsum_neg_distrib {G : Type u_1} {α : Sort u_4} [SubtractionCommMonoid G] (f : α → G) : (finsum fun (x : α) => -f x) = -finsum fun (x : α) => f x

theorem finprod_inv_distrib {G : Type u_1} {α : Sort u_4} [DivisionCommMonoid G] (f : α → G) : (finprod fun (x : α) => (f x)⁻¹) = (finprod fun (x : α) => f x)⁻¹

theorem finsum_eq_indicator_apply {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (s : Set α) (f : α → M) (a : α) : (finsum fun (x : a ∈ s) => f a) = Set.indicator s f a

theorem finprod_eq_mulIndicator_apply {α : Type u_1} {M : Type u_5} [CommMonoid M] (s : Set α) (f : α → M) (a : α) : (finprod fun (x : a ∈ s) => f a) = Set.mulIndicator s f a

@[simp]

theorem finsum_mem_support {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) (a : α) : (finsum fun (x : f a ≠ 0) => f a) = f a

@[simp]

theorem finprod_mem_mulSupport {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) (a : α) : (finprod fun (x : f a ≠ 1) => f a) = f a

theorem finsum_mem_def {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (s : Set α) (f : α → M) : (finsum fun (a : α) => finsum fun (h : a ∈ s) => f a) = finsum fun (a : α) => Set.indicator s f a

theorem finprod_mem_def {α : Type u_1} {M : Type u_5} [CommMonoid M] (s : Set α) (f : α → M) : (finprod fun (a : α) => finprod fun (h : a ∈ s) => f a) = finprod fun (a : α) => Set.mulIndicator s f a

theorem finsum_eq_sum_of_support_subset {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) {s : Finset α} (h : Function.support f ⊆ ↑s) : (finsum fun (i : α) => f i) = Finset.sum s fun (i : α) => f i

theorem finprod_eq_prod_of_mulSupport_subset {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) {s : Finset α} (h : Function.mulSupport f ⊆ ↑s) : (finprod fun (i : α) => f i) = Finset.prod s fun (i : α) => f i

theorem finsum_eq_sum_of_support_toFinset_subset {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) (hf : Set.Finite (Function.support f)) {s : Finset α} (h : Set.Finite.toFinset hf ⊆ s) : (finsum fun (i : α) => f i) = Finset.sum s fun (i : α) => f i

theorem finprod_eq_prod_of_mulSupport_toFinset_subset {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) (hf : Set.Finite (Function.mulSupport f)) {s : Finset α} (h : Set.Finite.toFinset hf ⊆ s) : (finprod fun (i : α) => f i) = Finset.prod s fun (i : α) => f i

theorem finsum_eq_finset_sum_of_support_subset {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) {s : Finset α} (h : Function.support f ⊆ ↑s) : (finsum fun (i : α) => f i) = Finset.sum s fun (i : α) => f i

theorem finprod_eq_finset_prod_of_mulSupport_subset {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) {s : Finset α} (h : Function.mulSupport f ⊆ ↑s) : (finprod fun (i : α) => f i) = Finset.prod s fun (i : α) => f i

theorem finsum_def {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) [Decidable (Set.Finite (Function.support f))] : (finsum fun (i : α) => f i) = if h : Set.Finite (Function.support f) then Finset.sum (Set.Finite.toFinset h) fun (i : α) => f i else 0

theorem finprod_def {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) [Decidable (Set.Finite (Function.mulSupport f))] : (finprod fun (i : α) => f i) = if h : Set.Finite (Function.mulSupport f) then Finset.prod (Set.Finite.toFinset h) fun (i : α) => f i else 1

theorem finsum_of_infinite_support {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} (hf : Set.Infinite (Function.support f)) : (finsum fun (i : α) => f i) = 0

theorem finprod_of_infinite_mulSupport {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} (hf : Set.Infinite (Function.mulSupport f)) : (finprod fun (i : α) => f i) = 1

theorem finsum_eq_sum {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) (hf : Set.Finite (Function.support f)) : (finsum fun (i : α) => f i) = Finset.sum (Set.Finite.toFinset hf) fun (i : α) => f i

theorem finprod_eq_prod {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) (hf : Set.Finite (Function.mulSupport f)) : (finprod fun (i : α) => f i) = Finset.prod (Set.Finite.toFinset hf) fun (i : α) => f i

theorem finsum_eq_sum_of_fintype {α : Type u_1} {M : Type u_5} [AddCommMonoid M] [Fintype α] (f : α → M) : (finsum fun (i : α) => f i) = Finset.sum Finset.univ fun (i : α) => f i

theorem finprod_eq_prod_of_fintype {α : Type u_1} {M : Type u_5} [CommMonoid M] [Fintype α] (f : α → M) : (finprod fun (i : α) => f i) = Finset.prod Finset.univ fun (i : α) => f i

theorem finsum_cond_eq_sum_of_cond_iff {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) {p : α → Prop} {t : Finset α} (h : ∀ {x : α}, f x ≠ 0 → (p x ↔ x ∈ t)) : (finsum fun (i : α) => finsum fun (x : p i) => f i) = Finset.sum t fun (i : α) => f i

theorem finprod_cond_eq_prod_of_cond_iff {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) {p : α → Prop} {t : Finset α} (h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)) : (finprod fun (i : α) => finprod fun (x : p i) => f i) = Finset.prod t fun (i : α) => f i

theorem finsum_cond_ne {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) (a : α) [DecidableEq α] (hf : Set.Finite (Function.support f)) : (finsum fun (i : α) => finsum fun (x : i ≠ a) => f i) = Finset.sum (Finset.erase (Set.Finite.toFinset hf) a) fun (i : α) => f i

theorem finprod_cond_ne {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) (a : α) [DecidableEq α] (hf : Set.Finite (Function.mulSupport f)) : (finprod fun (i : α) => finprod fun (x : i ≠ a) => f i) = Finset.prod (Finset.erase (Set.Finite.toFinset hf) a) fun (i : α) => f i

theorem finsum_mem_eq_sum_of_inter_support_eq {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) {s : Set α} {t : Finset α} (h : s ∩ Function.support f = ↑t ∩ Function.support f) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) = Finset.sum t fun (i : α) => f i

theorem finprod_mem_eq_prod_of_inter_mulSupport_eq {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) {s : Set α} {t : Finset α} (h : s ∩ Function.mulSupport f = ↑t ∩ Function.mulSupport f) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) = Finset.prod t fun (i : α) => f i

theorem finsum_mem_eq_sum_of_subset {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) {s : Set α} {t : Finset α} (h₁ : s ∩ Function.support f ⊆ ↑t) (h₂ : ↑t ⊆ s) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) = Finset.sum t fun (i : α) => f i

theorem finprod_mem_eq_prod_of_subset {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) {s : Set α} {t : Finset α} (h₁ : s ∩ Function.mulSupport f ⊆ ↑t) (h₂ : ↑t ⊆ s) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) = Finset.prod t fun (i : α) => f i

theorem finsum_mem_eq_sum {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) {s : Set α} (hf : Set.Finite (s ∩ Function.support f)) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) = Finset.sum (Set.Finite.toFinset hf) fun (i : α) => f i

theorem finprod_mem_eq_prod {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) {s : Set α} (hf : Set.Finite (s ∩ Function.mulSupport f)) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) = Finset.prod (Set.Finite.toFinset hf) fun (i : α) => f i

theorem finsum_mem_eq_sum_filter {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) (s : Set α) [DecidablePred fun (x : α) => x ∈ s] (hf : Set.Finite (Function.support f)) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) = Finset.sum (Finset.filter (fun (x : α) => x ∈ s) (Set.Finite.toFinset hf)) fun (i : α) => f i

theorem finprod_mem_eq_prod_filter {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) (s : Set α) [DecidablePred fun (x : α) => x ∈ s] (hf : Set.Finite (Function.mulSupport f)) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) = Finset.prod (Finset.filter (fun (x : α) => x ∈ s) (Set.Finite.toFinset hf)) fun (i : α) => f i

theorem finsum_mem_eq_toFinset_sum {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) (s : Set α) [Fintype ↑s] : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) = Finset.sum (Set.toFinset s) fun (i : α) => f i

theorem finprod_mem_eq_toFinset_prod {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) (s : Set α) [Fintype ↑s] : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) = Finset.prod (Set.toFinset s) fun (i : α) => f i

theorem finsum_mem_eq_finite_toFinset_sum {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) {s : Set α} (hs : Set.Finite s) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) = Finset.sum (Set.Finite.toFinset hs) fun (i : α) => f i

theorem finprod_mem_eq_finite_toFinset_prod {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) {s : Set α} (hs : Set.Finite s) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) = Finset.prod (Set.Finite.toFinset hs) fun (i : α) => f i

theorem finsum_mem_finset_eq_sum {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) (s : Finset α) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) = Finset.sum s fun (i : α) => f i

theorem finprod_mem_finset_eq_prod {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) (s : Finset α) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) = Finset.prod s fun (i : α) => f i

theorem finsum_mem_coe_finset {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) (s : Finset α) : (finsum fun (i : α) => finsum fun (h : i ∈ ↑s) => f i) = Finset.sum s fun (i : α) => f i

theorem finprod_mem_coe_finset {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) (s : Finset α) : (finprod fun (i : α) => finprod fun (h : i ∈ ↑s) => f i) = Finset.prod s fun (i : α) => f i

theorem finsum_mem_eq_zero_of_infinite {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set α} (hs : Set.Infinite (s ∩ Function.support f)) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) = 0

theorem finprod_mem_eq_one_of_infinite {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set α} (hs : Set.Infinite (s ∩ Function.mulSupport f)) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) = 1

theorem finsum_mem_eq_zero_of_forall_eq_zero {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set α} (h : ∀ x ∈ s, f x = 0) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) = 0

theorem finprod_mem_eq_one_of_forall_eq_one {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set α} (h : ∀ x ∈ s, f x = 1) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) = 1

theorem finsum_mem_inter_support {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) (s : Set α) : (finsum fun (i : α) => finsum fun (h : i ∈ s ∩ Function.support f) => f i) = finsum fun (i : α) => finsum fun (h : i ∈ s) => f i

theorem finprod_mem_inter_mulSupport {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) (s : Set α) : (finprod fun (i : α) => finprod fun (h : i ∈ s ∩ Function.mulSupport f) => f i) = finprod fun (i : α) => finprod fun (h : i ∈ s) => f i

theorem finsum_mem_inter_support_eq {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) (s : Set α) (t : Set α) (h : s ∩ Function.support f = t ∩ Function.support f) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) = finsum fun (i : α) => finsum fun (h : i ∈ t) => f i

theorem finprod_mem_inter_mulSupport_eq {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) (s : Set α) (t : Set α) (h : s ∩ Function.mulSupport f = t ∩ Function.mulSupport f) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) = finprod fun (i : α) => finprod fun (h : i ∈ t) => f i

theorem finsum_mem_inter_support_eq' {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) (s : Set α) (t : Set α) (h : ∀ x ∈ Function.support f, x ∈ s ↔ x ∈ t) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) = finsum fun (i : α) => finsum fun (h : i ∈ t) => f i

theorem finprod_mem_inter_mulSupport_eq' {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) (s : Set α) (t : Set α) (h : ∀ x ∈ Function.mulSupport f, x ∈ s ↔ x ∈ t) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) = finprod fun (i : α) => finprod fun (h : i ∈ t) => f i

theorem finsum_mem_univ {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : α → M) : (finsum fun (i : α) => finsum fun (h : i ∈ Set.univ) => f i) = finsum fun (i : α) => f i

theorem finprod_mem_univ {α : Type u_1} {M : Type u_5} [CommMonoid M] (f : α → M) : (finprod fun (i : α) => finprod fun (h : i ∈ Set.univ) => f i) = finprod fun (i : α) => f i

theorem finsum_mem_congr {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {g : α → M} {s : Set α} {t : Set α} (h₀ : s = t) (h₁ : ∀ x ∈ t, f x = g x) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) = finsum fun (i : α) => finsum fun (h : i ∈ t) => g i

theorem finprod_mem_congr {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {g : α → M} {s : Set α} {t : Set α} (h₀ : s = t) (h₁ : ∀ x ∈ t, f x = g x) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) = finprod fun (i : α) => finprod fun (h : i ∈ t) => g i

theorem finsum_eq_zero_of_forall_eq_zero {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} (h : ∀ (x : α), f x = 0) : (finsum fun (i : α) => f i) = 0

theorem finprod_eq_one_of_forall_eq_one {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} (h : ∀ (x : α), f x = 1) : (finprod fun (i : α) => f i) = 1

theorem finsum_pos' {ι : Type u_3} {M : Type u_7} [OrderedCancelAddCommMonoid M] {f : ι → M} (h : ∀ (i : ι), 0 ≤ f i) (h' : ∃ (i : ι), 0 < f i) (hf : Set.Finite (Function.support f)) : 0 < finsum fun (i : ι) => f i

theorem one_lt_finprod' {ι : Type u_3} {M : Type u_7} [OrderedCancelCommMonoid M] {f : ι → M} (h : ∀ (i : ι), 1 ≤ f i) (h' : ∃ (i : ι), 1 < f i) (hf : Set.Finite (Function.mulSupport f)) : 1 < finprod fun (i : ι) => f i

Distributivity w.r.t. addition, subtraction, and (scalar) multiplication

theorem finsum_add_distrib {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {g : α → M} (hf : Set.Finite (Function.support f)) (hg : Set.Finite (Function.support g)) : (finsum fun (i : α) => f i + g i) = (finsum fun (i : α) => f i) + finsum fun (i : α) => g i

If the additive supports of f and g are finite, then the sum of f i + g i equals the sum of f i plus the sum of g i.

theorem finprod_mul_distrib {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {g : α → M} (hf : Set.Finite (Function.mulSupport f)) (hg : Set.Finite (Function.mulSupport g)) : (finprod fun (i : α) => f i * g i) = (finprod fun (i : α) => f i) * finprod fun (i : α) => g i

If the multiplicative supports of f and g are finite, then the product of f i * g i equals the product of f i multiplied by the product of g i.

theorem finsum_sub_distrib {α : Type u_1} {G : Type u_4} [SubtractionCommMonoid G] {f : α → G} {g : α → G} (hf : Set.Finite (Function.support f)) (hg : Set.Finite (Function.support g)) : (finsum fun (i : α) => f i - g i) = (finsum fun (i : α) => f i) - finsum fun (i : α) => g i

If the additive supports of f and g are finite, then the sum of f i - g i equals the sum of f i minus the sum of g i.

theorem finprod_div_distrib {α : Type u_1} {G : Type u_4} [DivisionCommMonoid G] {f : α → G} {g : α → G} (hf : Set.Finite (Function.mulSupport f)) (hg : Set.Finite (Function.mulSupport g)) : (finprod fun (i : α) => f i / g i) = (finprod fun (i : α) => f i) / finprod fun (i : α) => g i

If the multiplicative supports of f and g are finite, then the product of f i / g i equals the product of f i divided by the product of g i.

theorem finsum_mem_add_distrib' {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {g : α → M} {s : Set α} (hf : Set.Finite (s ∩ Function.support f)) (hg : Set.Finite (s ∩ Function.support g)) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i + g i) = (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) + finsum fun (i : α) => finsum fun (h : i ∈ s) => g i

A more general version of finsum_mem_add_distrib that only requires s ∩ support f and s ∩ support g rather than s to be finite.

theorem finprod_mem_mul_distrib' {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {g : α → M} {s : Set α} (hf : Set.Finite (s ∩ Function.mulSupport f)) (hg : Set.Finite (s ∩ Function.mulSupport g)) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i * g i) = (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) * finprod fun (i : α) => finprod fun (h : i ∈ s) => g i

A more general version of finprod_mem_mul_distrib that only requires s ∩ mulSupport f and s ∩ mulSupport g rather than s to be finite.

theorem finsum_mem_zero {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (s : Set α) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => 0) = 0

The sum of the constant function 0 over any set equals 0.

theorem finprod_mem_one {α : Type u_1} {M : Type u_5} [CommMonoid M] (s : Set α) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => 1) = 1

The product of the constant function 1 over any set equals 1.

theorem finsum_mem_of_eqOn_zero {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set α} (hf : Set.EqOn f 0 s) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) = 0

If a function f equals 0 on a set s, then the product of f i over i ∈ s equals 0.

theorem finprod_mem_of_eqOn_one {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set α} (hf : Set.EqOn f 1 s) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) = 1

If a function f equals 1 on a set s, then the product of f i over i ∈ s equals 1.

theorem exists_ne_zero_of_finsum_mem_ne_zero {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set α} (h : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) ≠ 0) : ∃ x ∈ s, f x ≠ 0

If the product of f i over i ∈ s is not equal to 0, then there is some x ∈ s such that f x ≠ 0.

theorem exists_ne_one_of_finprod_mem_ne_one {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set α} (h : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) ≠ 1) : ∃ x ∈ s, f x ≠ 1

If the product of f i over i ∈ s is not equal to 1, then there is some x ∈ s such that f x ≠ 1.

theorem finsum_mem_add_distrib {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {g : α → M} {s : Set α} (hs : Set.Finite s) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i + g i) = (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) + finsum fun (i : α) => finsum fun (h : i ∈ s) => g i

Given a finite set s, the sum of f i + g i over i ∈ s equals the sum of f i over i ∈ s plus the sum of g i over i ∈ s.

theorem finprod_mem_mul_distrib {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {g : α → M} {s : Set α} (hs : Set.Finite s) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i * g i) = (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) * finprod fun (i : α) => finprod fun (h : i ∈ s) => g i

Given a finite set s, the product of f i * g i over i ∈ s equals the product of f i over i ∈ s times the product of g i over i ∈ s.

theorem AddMonoidHom.map_finsum {α : Type u_1} {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] {f : α → M} (g : M →+ N) (hf : Set.Finite (Function.support f)) : g (finsum fun (i : α) => f i) = finsum fun (i : α) => g (f i)

theorem MonoidHom.map_finprod {α : Type u_1} {M : Type u_5} {N : Type u_6} [CommMonoid M] [CommMonoid N] {f : α → M} (g : M →* N) (hf : Set.Finite (Function.mulSupport f)) : g (finprod fun (i : α) => f i) = finprod fun (i : α) => g (f i)

theorem finsum_nsmul {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} (hf : Set.Finite (Function.support f)) (n : ℕ) : (n • finsum fun (i : α) => f i) = finsum fun (i : α) => n • f i

theorem finprod_pow {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} (hf : Set.Finite (Function.mulSupport f)) (n : ℕ) : (finprod fun (i : α) => f i) ^ n = finprod fun (i : α) => f i ^ n

theorem finsum_smul' {ι : Type u_3} {R : Type u_7} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] {f : ι → R} (hf : Set.Finite (Function.support f)) (x : M) : (finsum fun (i : ι) => f i) • x = finsum fun (i : ι) => f i • x

See also finsum_smul for a version that works even when the support of f is not finite, but with slightly stronger typeclass requirements.

theorem smul_finsum' {ι : Type u_3} {R : Type u_7} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] (c : R) {f : ι → M} (hf : Set.Finite (Function.support f)) : (c • finsum fun (i : ι) => f i) = finsum fun (i : ι) => c • f i

See also smul_finsum for a version that works even when the support of f is not finite, but with slightly stronger typeclass requirements.

theorem AddMonoidHom.map_finsum_mem' {α : Type u_1} {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] {s : Set α} {f : α → M} (g : M →+ N) (h₀ : Set.Finite (s ∩ Function.support f)) : g (finsum fun (j : α) => finsum fun (h : j ∈ s) => f j) = finsum fun (i : α) => finsum fun (h : i ∈ s) => g (f i)

A more general version of AddMonoidHom.map_finsum_mem that requires s ∩ support f rather than s to be finite.

theorem MonoidHom.map_finprod_mem' {α : Type u_1} {M : Type u_5} {N : Type u_6} [CommMonoid M] [CommMonoid N] {s : Set α} {f : α → M} (g : M →* N) (h₀ : Set.Finite (s ∩ Function.mulSupport f)) : g (finprod fun (j : α) => finprod fun (h : j ∈ s) => f j) = finprod fun (i : α) => finprod fun (h : i ∈ s) => g (f i)

A more general version of MonoidHom.map_finprod_mem that requires s ∩ mulSupport f rather than s to be finite.

theorem AddMonoidHom.map_finsum_mem {α : Type u_1} {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] {s : Set α} (f : α → M) (g : M →+ N) (hs : Set.Finite s) : g (finsum fun (j : α) => finsum fun (h : j ∈ s) => f j) = finsum fun (i : α) => finsum fun (h : i ∈ s) => g (f i)

Given an additive monoid homomorphism g : M →* N and a function f : α → M, the value of g at the sum of f i over i ∈ s equals the sum of g (f i) over s.

theorem MonoidHom.map_finprod_mem {α : Type u_1} {M : Type u_5} {N : Type u_6} [CommMonoid M] [CommMonoid N] {s : Set α} (f : α → M) (g : M →* N) (hs : Set.Finite s) : g (finprod fun (j : α) => finprod fun (h : j ∈ s) => f j) = finprod fun (i : α) => finprod fun (h : i ∈ s) => g (f i)

Given a monoid homomorphism g : M →* N and a function f : α → M, the value of g at the product of f i over i ∈ s equals the product of g (f i) over s.

theorem AddEquiv.map_finsum_mem {α : Type u_1} {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] (g : M ≃+ N) (f : α → M) {s : Set α} (hs : Set.Finite s) : g (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) = finsum fun (i : α) => finsum fun (h : i ∈ s) => g (f i)

theorem MulEquiv.map_finprod_mem {α : Type u_1} {M : Type u_5} {N : Type u_6} [CommMonoid M] [CommMonoid N] (g : M ≃* N) (f : α → M) {s : Set α} (hs : Set.Finite s) : g (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) = finprod fun (i : α) => finprod fun (h : i ∈ s) => g (f i)

theorem finsum_mem_neg_distrib {α : Type u_1} {G : Type u_4} {s : Set α} [SubtractionCommMonoid G] (f : α → G) (hs : Set.Finite s) : (finsum fun (x : α) => finsum fun (h : x ∈ s) => -f x) = -finsum fun (x : α) => finsum fun (h : x ∈ s) => f x

theorem finprod_mem_inv_distrib {α : Type u_1} {G : Type u_4} {s : Set α} [DivisionCommMonoid G] (f : α → G) (hs : Set.Finite s) : (finprod fun (x : α) => finprod fun (h : x ∈ s) => (f x)⁻¹) = (finprod fun (x : α) => finprod fun (h : x ∈ s) => f x)⁻¹

theorem finsum_mem_sub_distrib {α : Type u_1} {G : Type u_4} {s : Set α} [SubtractionCommMonoid G] (f : α → G) (g : α → G) (hs : Set.Finite s) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i - g i) = (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) - finsum fun (i : α) => finsum fun (h : i ∈ s) => g i

Given a finite set s, the sum of f i / g i over i ∈ s equals the sum of f i over i ∈ s minus the sum of g i over i ∈ s.

theorem finprod_mem_div_distrib {α : Type u_1} {G : Type u_4} {s : Set α} [DivisionCommMonoid G] (f : α → G) (g : α → G) (hs : Set.Finite s) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i / g i) = (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) / finprod fun (i : α) => finprod fun (h : i ∈ s) => g i

Given a finite set s, the product of f i / g i over i ∈ s equals the product of f i over i ∈ s divided by the product of g i over i ∈ s.

∏ᶠ x ∈ s, f x and set operations

theorem finsum_mem_empty {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} : (finsum fun (i : α) => finsum fun (h : i ∈ ∅) => f i) = 0

The sum of any function over an empty set is 0.

theorem finprod_mem_empty {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} : (finprod fun (i : α) => finprod fun (h : i ∈ ∅) => f i) = 1

The product of any function over an empty set is 1.

theorem nonempty_of_finsum_mem_ne_zero {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set α} (h : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) ≠ 0) : Set.Nonempty s

A set s is nonempty if the sum of some function over s is not equal to 0.

theorem nonempty_of_finprod_mem_ne_one {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set α} (h : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) ≠ 1) : Set.Nonempty s

A set s is nonempty if the product of some function over s is not equal to 1.

theorem finsum_mem_union_inter {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set α} {t : Set α} (hs : Set.Finite s) (ht : Set.Finite t) : ((finsum fun (i : α) => finsum fun (h : i ∈ s ∪ t) => f i) + finsum fun (i : α) => finsum fun (h : i ∈ s ∩ t) => f i) = (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) + finsum fun (i : α) => finsum fun (h : i ∈ t) => f i

Given finite sets s and t, the sum of f i over i ∈ s ∪ t plus the sum of f i over i ∈ s ∩ t equals the sum of f i over i ∈ s plus the sum of f i over i ∈ t.

theorem finprod_mem_union_inter {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set α} {t : Set α} (hs : Set.Finite s) (ht : Set.Finite t) : ((finprod fun (i : α) => finprod fun (h : i ∈ s ∪ t) => f i) * finprod fun (i : α) => finprod fun (h : i ∈ s ∩ t) => f i) = (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) * finprod fun (i : α) => finprod fun (h : i ∈ t) => f i

Given finite sets s and t, the product of f i over i ∈ s ∪ t times the product of f i over i ∈ s ∩ t equals the product of f i over i ∈ s times the product of f i over i ∈ t.

theorem finsum_mem_union_inter' {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set α} {t : Set α} (hs : Set.Finite (s ∩ Function.support f)) (ht : Set.Finite (t ∩ Function.support f)) : ((finsum fun (i : α) => finsum fun (h : i ∈ s ∪ t) => f i) + finsum fun (i : α) => finsum fun (h : i ∈ s ∩ t) => f i) = (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) + finsum fun (i : α) => finsum fun (h : i ∈ t) => f i

A more general version of finsum_mem_union_inter that requires s ∩ support f and t ∩ support f rather than s and t to be finite.

theorem finprod_mem_union_inter' {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set α} {t : Set α} (hs : Set.Finite (s ∩ Function.mulSupport f)) (ht : Set.Finite (t ∩ Function.mulSupport f)) : ((finprod fun (i : α) => finprod fun (h : i ∈ s ∪ t) => f i) * finprod fun (i : α) => finprod fun (h : i ∈ s ∩ t) => f i) = (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) * finprod fun (i : α) => finprod fun (h : i ∈ t) => f i

A more general version of finprod_mem_union_inter that requires s ∩ mulSupport f and t ∩ mulSupport f rather than s and t to be finite.

theorem finsum_mem_union' {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set α} {t : Set α} (hst : Disjoint s t) (hs : Set.Finite (s ∩ Function.support f)) (ht : Set.Finite (t ∩ Function.support f)) : (finsum fun (i : α) => finsum fun (h : i ∈ s ∪ t) => f i) = (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) + finsum fun (i : α) => finsum fun (h : i ∈ t) => f i

A more general version of finsum_mem_union that requires s ∩ support f and t ∩ support f rather than s and t to be finite.

theorem finprod_mem_union' {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set α} {t : Set α} (hst : Disjoint s t) (hs : Set.Finite (s ∩ Function.mulSupport f)) (ht : Set.Finite (t ∩ Function.mulSupport f)) : (finprod fun (i : α) => finprod fun (h : i ∈ s ∪ t) => f i) = (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) * finprod fun (i : α) => finprod fun (h : i ∈ t) => f i

A more general version of finprod_mem_union that requires s ∩ mulSupport f and t ∩ mulSupport f rather than s and t to be finite.

theorem finsum_mem_union {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set α} {t : Set α} (hst : Disjoint s t) (hs : Set.Finite s) (ht : Set.Finite t) : (finsum fun (i : α) => finsum fun (h : i ∈ s ∪ t) => f i) = (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) + finsum fun (i : α) => finsum fun (h : i ∈ t) => f i

Given two finite disjoint sets s and t, the sum of f i over i ∈ s ∪ t equals the sum of f i over i ∈ s plus the sum of f i over i ∈ t.

theorem finprod_mem_union {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set α} {t : Set α} (hst : Disjoint s t) (hs : Set.Finite s) (ht : Set.Finite t) : (finprod fun (i : α) => finprod fun (h : i ∈ s ∪ t) => f i) = (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) * finprod fun (i : α) => finprod fun (h : i ∈ t) => f i

Given two finite disjoint sets s and t, the product of f i over i ∈ s ∪ t equals the product of f i over i ∈ s times the product of f i over i ∈ t.

theorem finsum_mem_union'' {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set α} {t : Set α} (hst : Disjoint (s ∩ Function.support f) (t ∩ Function.support f)) (hs : Set.Finite (s ∩ Function.support f)) (ht : Set.Finite (t ∩ Function.support f)) : (finsum fun (i : α) => finsum fun (h : i ∈ s ∪ t) => f i) = (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) + finsum fun (i : α) => finsum fun (h : i ∈ t) => f i

A more general version of finsum_mem_union' that requires s ∩ support f and t ∩ support f rather than s and t to be disjoint

theorem finprod_mem_union'' {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set α} {t : Set α} (hst : Disjoint (s ∩ Function.mulSupport f) (t ∩ Function.mulSupport f)) (hs : Set.Finite (s ∩ Function.mulSupport f)) (ht : Set.Finite (t ∩ Function.mulSupport f)) : (finprod fun (i : α) => finprod fun (h : i ∈ s ∪ t) => f i) = (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) * finprod fun (i : α) => finprod fun (h : i ∈ t) => f i

A more general version of finprod_mem_union' that requires s ∩ mulSupport f and t ∩ mulSupport f rather than s and t to be disjoint

theorem finsum_mem_singleton {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {a : α} : (finsum fun (i : α) => finsum fun (h : i ∈ {a}) => f i) = f a

The sum of f i over i ∈ {a} equals f a.

theorem finprod_mem_singleton {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {a : α} : (finprod fun (i : α) => finprod fun (h : i ∈ {a}) => f i) = f a

The product of f i over i ∈ {a} equals f a.

@[simp]

theorem finsum_cond_eq_left {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {a : α} : (finsum fun (i : α) => finsum fun (x : i = a) => f i) = f a

@[simp]

theorem finprod_cond_eq_left {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {a : α} : (finprod fun (i : α) => finprod fun (x : i = a) => f i) = f a

@[simp]

theorem finsum_cond_eq_right {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {a : α} : (finsum fun (i : α) => finsum fun (x : a = i) => f i) = f a

@[simp]

theorem finprod_cond_eq_right {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {a : α} : (finprod fun (i : α) => finprod fun (x : a = i) => f i) = f a

theorem finsum_mem_insert' {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {a : α} {s : Set α} (f : α → M) (h : a ∉ s) (hs : Set.Finite (s ∩ Function.support f)) : (finsum fun (i : α) => finsum fun (h : i ∈ insert a s) => f i) = f a + finsum fun (i : α) => finsum fun (h : i ∈ s) => f i

A more general version of finsum_mem_insert that requires s ∩ support f rather than s to be finite.

theorem finprod_mem_insert' {α : Type u_1} {M : Type u_5} [CommMonoid M] {a : α} {s : Set α} (f : α → M) (h : a ∉ s) (hs : Set.Finite (s ∩ Function.mulSupport f)) : (finprod fun (i : α) => finprod fun (h : i ∈ insert a s) => f i) = f a * finprod fun (i : α) => finprod fun (h : i ∈ s) => f i

A more general version of finprod_mem_insert that requires s ∩ mulSupport f rather than s to be finite.

theorem finsum_mem_insert {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {a : α} {s : Set α} (f : α → M) (h : a ∉ s) (hs : Set.Finite s) : (finsum fun (i : α) => finsum fun (h : i ∈ insert a s) => f i) = f a + finsum fun (i : α) => finsum fun (h : i ∈ s) => f i

Given a finite set s and an element a ∉ s, the sum of f i over i ∈ insert a s equals f a plus the sum of f i over i ∈ s.

theorem finprod_mem_insert {α : Type u_1} {M : Type u_5} [CommMonoid M] {a : α} {s : Set α} (f : α → M) (h : a ∉ s) (hs : Set.Finite s) : (finprod fun (i : α) => finprod fun (h : i ∈ insert a s) => f i) = f a * finprod fun (i : α) => finprod fun (h : i ∈ s) => f i

Given a finite set s and an element a ∉ s, the product of f i over i ∈ insert a s equals f a times the product of f i over i ∈ s.

theorem finsum_mem_insert_of_eq_zero_if_not_mem {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {a : α} {s : Set α} (h : a ∉ s → f a = 0) : (finsum fun (i : α) => finsum fun (h : i ∈ insert a s) => f i) = finsum fun (i : α) => finsum fun (h : i ∈ s) => f i

If f a = 0 when a ∉ s, then the sum of f i over i ∈ insert a s equals the sum of f i over i ∈ s.

theorem finprod_mem_insert_of_eq_one_if_not_mem {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {a : α} {s : Set α} (h : a ∉ s → f a = 1) : (finprod fun (i : α) => finprod fun (h : i ∈ insert a s) => f i) = finprod fun (i : α) => finprod fun (h : i ∈ s) => f i

If f a = 1 when a ∉ s, then the product of f i over i ∈ insert a s equals the product of f i over i ∈ s.

theorem finsum_mem_insert_zero {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {a : α} {s : Set α} (h : f a = 0) : (finsum fun (i : α) => finsum fun (h : i ∈ insert a s) => f i) = finsum fun (i : α) => finsum fun (h : i ∈ s) => f i

If f a = 0, then the sum of f i over i ∈ insert a s equals the sum of f i over i ∈ s.

theorem finprod_mem_insert_one {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {a : α} {s : Set α} (h : f a = 1) : (finprod fun (i : α) => finprod fun (h : i ∈ insert a s) => f i) = finprod fun (i : α) => finprod fun (h : i ∈ s) => f i

If f a = 1, then the product of f i over i ∈ insert a s equals the product of f i over i ∈ s.

theorem finprod_mem_dvd {α : Type u_1} {N : Type u_6} [CommMonoid N] {f : α → N} (a : α) (hf : Set.Finite (Function.mulSupport f)) : f a ∣ finprod f

If the multiplicative support of f is finite, then for every x in the domain of f, f x divides finprod f.

theorem finsum_mem_pair {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {a : α} {b : α} (h : a ≠ b) : (finsum fun (i : α) => finsum fun (h : i ∈ {a, b}) => f i) = f a + f b

The sum of f i over i ∈ {a, b}, a ≠ b, is equal to f a + f b.

theorem finprod_mem_pair {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {a : α} {b : α} (h : a ≠ b) : (finprod fun (i : α) => finprod fun (h : i ∈ {a, b}) => f i) = f a * f b

The product of f i over i ∈ {a, b}, a ≠ b, is equal to f a * f b.

theorem finsum_mem_image' {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set β} {g : β → α} (hg : Set.InjOn g (s ∩ Function.support (f ∘ g))) : (finsum fun (i : α) => finsum fun (h : i ∈ g '' s) => f i) = finsum fun (j : β) => finsum fun (h : j ∈ s) => f (g j)

The sum of f y over y ∈ g '' s equals the sum of f (g i) over s provided that g is injective on s ∩ support (f ∘ g).

theorem finprod_mem_image' {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set β} {g : β → α} (hg : Set.InjOn g (s ∩ Function.mulSupport (f ∘ g))) : (finprod fun (i : α) => finprod fun (h : i ∈ g '' s) => f i) = finprod fun (j : β) => finprod fun (h : j ∈ s) => f (g j)

The product of f y over y ∈ g '' s equals the product of f (g i) over s provided that g is injective on s ∩ mulSupport (f ∘ g).

theorem finsum_mem_image {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set β} {g : β → α} (hg : Set.InjOn g s) : (finsum fun (i : α) => finsum fun (h : i ∈ g '' s) => f i) = finsum fun (j : β) => finsum fun (h : j ∈ s) => f (g j)

The sum of f y over y ∈ g '' s equals the sum of f (g i) over s provided that g is injective on s.

theorem finprod_mem_image {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set β} {g : β → α} (hg : Set.InjOn g s) : (finprod fun (i : α) => finprod fun (h : i ∈ g '' s) => f i) = finprod fun (j : β) => finprod fun (h : j ∈ s) => f (g j)

The product of f y over y ∈ g '' s equals the product of f (g i) over s provided that g is injective on s.

theorem finsum_mem_range' {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : α → M} {g : β → α} (hg : Set.InjOn g (Function.support (f ∘ g))) : (finsum fun (i : α) => finsum fun (h : i ∈ Set.range g) => f i) = finsum fun (j : β) => f (g j)

The sum of f y over y ∈ Set.range g equals the sum of f (g i) over all i provided that g is injective on support (f ∘ g).

theorem finprod_mem_range' {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] {f : α → M} {g : β → α} (hg : Set.InjOn g (Function.mulSupport (f ∘ g))) : (finprod fun (i : α) => finprod fun (h : i ∈ Set.range g) => f i) = finprod fun (j : β) => f (g j)

The product of f y over y ∈ Set.range g equals the product of f (g i) over all i provided that g is injective on mulSupport (f ∘ g).

theorem finsum_mem_range {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : α → M} {g : β → α} (hg : Function.Injective g) : (finsum fun (i : α) => finsum fun (h : i ∈ Set.range g) => f i) = finsum fun (j : β) => f (g j)

The sum of f y over y ∈ Set.range g equals the sum of f (g i) over all i provided that g is injective.

theorem finprod_mem_range {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] {f : α → M} {g : β → α} (hg : Function.Injective g) : (finprod fun (i : α) => finprod fun (h : i ∈ Set.range g) => f i) = finprod fun (j : β) => f (g j)

The product of f y over y ∈ Set.range g equals the product of f (g i) over all i provided that g is injective.

theorem finsum_mem_eq_of_bijOn {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {s : Set α} {t : Set β} {f : α → M} {g : β → M} (e : α → β) (he₀ : Set.BijOn e s t) (he₁ : ∀ x ∈ s, f x = g (e x)) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) = finsum fun (j : β) => finsum fun (h : j ∈ t) => g j

See also Finset.sum_bij.

theorem finprod_mem_eq_of_bijOn {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] {s : Set α} {t : Set β} {f : α → M} {g : β → M} (e : α → β) (he₀ : Set.BijOn e s t) (he₁ : ∀ x ∈ s, f x = g (e x)) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) = finprod fun (j : β) => finprod fun (h : j ∈ t) => g j

See also Finset.prod_bij.

theorem finsum_eq_of_bijective {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : α → M} {g : β → M} (e : α → β) (he₀ : Function.Bijective e) (he₁ : ∀ (x : α), f x = g (e x)) : (finsum fun (i : α) => f i) = finsum fun (j : β) => g j

See finsum_comp, Fintype.sum_bijective and Finset.sum_bij.

theorem finprod_eq_of_bijective {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] {f : α → M} {g : β → M} (e : α → β) (he₀ : Function.Bijective e) (he₁ : ∀ (x : α), f x = g (e x)) : (finprod fun (i : α) => f i) = finprod fun (j : β) => g j

See finprod_comp, Fintype.prod_bijective and Finset.prod_bij.

theorem finsum_comp {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {g : β → M} (e : α → β) (he₀ : Function.Bijective e) : (finsum fun (i : α) => g (e i)) = finsum fun (j : β) => g j

See also finsum_eq_of_bijective, Fintype.sum_bijective and Finset.sum_bij.

theorem finprod_comp {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] {g : β → M} (e : α → β) (he₀ : Function.Bijective e) : (finprod fun (i : α) => g (e i)) = finprod fun (j : β) => g j

See also finprod_eq_of_bijective, Fintype.prod_bijective and Finset.prod_bij.

theorem finsum_comp_equiv {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (e : α ≃ β) {f : β → M} : (finsum fun (i : α) => f (e i)) = finsum fun (i' : β) => f i'

theorem finprod_comp_equiv {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] (e : α ≃ β) {f : β → M} : (finprod fun (i : α) => f (e i)) = finprod fun (i' : β) => f i'

theorem finsum_set_coe_eq_finsum_mem {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} (s : Set α) : (finsum fun (j : ↑s) => f ↑j) = finsum fun (i : α) => finsum fun (h : i ∈ s) => f i

theorem finprod_set_coe_eq_finprod_mem {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} (s : Set α) : (finprod fun (j : ↑s) => f ↑j) = finprod fun (i : α) => finprod fun (h : i ∈ s) => f i

theorem finsum_subtype_eq_finsum_cond {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} (p : α → Prop) : (finsum fun (j : Subtype p) => f ↑j) = finsum fun (i : α) => finsum fun (x : p i) => f i

theorem finprod_subtype_eq_finprod_cond {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} (p : α → Prop) : (finprod fun (j : Subtype p) => f ↑j) = finprod fun (i : α) => finprod fun (x : p i) => f i

theorem finsum_mem_inter_add_diff' {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set α} (t : Set α) (h : Set.Finite (s ∩ Function.support f)) : ((finsum fun (i : α) => finsum fun (h : i ∈ s ∩ t) => f i) + finsum fun (i : α) => finsum fun (h : i ∈ s \ t) => f i) = finsum fun (i : α) => finsum fun (h : i ∈ s) => f i

theorem finprod_mem_inter_mul_diff' {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set α} (t : Set α) (h : Set.Finite (s ∩ Function.mulSupport f)) : ((finprod fun (i : α) => finprod fun (h : i ∈ s ∩ t) => f i) * finprod fun (i : α) => finprod fun (h : i ∈ s \ t) => f i) = finprod fun (i : α) => finprod fun (h : i ∈ s) => f i

theorem finsum_mem_inter_add_diff {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set α} (t : Set α) (h : Set.Finite s) : ((finsum fun (i : α) => finsum fun (h : i ∈ s ∩ t) => f i) + finsum fun (i : α) => finsum fun (h : i ∈ s \ t) => f i) = finsum fun (i : α) => finsum fun (h : i ∈ s) => f i

theorem finprod_mem_inter_mul_diff {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set α} (t : Set α) (h : Set.Finite s) : ((finprod fun (i : α) => finprod fun (h : i ∈ s ∩ t) => f i) * finprod fun (i : α) => finprod fun (h : i ∈ s \ t) => f i) = finprod fun (i : α) => finprod fun (h : i ∈ s) => f i

theorem finsum_mem_add_diff' {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set α} {t : Set α} (hst : s ⊆ t) (ht : Set.Finite (t ∩ Function.support f)) : ((finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) + finsum fun (i : α) => finsum fun (h : i ∈ t \ s) => f i) = finsum fun (i : α) => finsum fun (h : i ∈ t) => f i

A more general version of finsum_mem_add_diff that requires t ∩ support f rather than t to be finite.

theorem finprod_mem_mul_diff' {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set α} {t : Set α} (hst : s ⊆ t) (ht : Set.Finite (t ∩ Function.mulSupport f)) : ((finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) * finprod fun (i : α) => finprod fun (h : i ∈ t \ s) => f i) = finprod fun (i : α) => finprod fun (h : i ∈ t) => f i

A more general version of finprod_mem_mul_diff that requires t ∩ mulSupport f rather than t to be finite.

theorem finsum_mem_add_diff {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set α} {t : Set α} (hst : s ⊆ t) (ht : Set.Finite t) : ((finsum fun (i : α) => finsum fun (h : i ∈ s) => f i) + finsum fun (i : α) => finsum fun (h : i ∈ t \ s) => f i) = finsum fun (i : α) => finsum fun (h : i ∈ t) => f i

Given a finite set t and a subset s of t, the sum of f i over i ∈ s plus the sum of f i over t \ s equals the sum of f i over i ∈ t.

theorem finprod_mem_mul_diff {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set α} {t : Set α} (hst : s ⊆ t) (ht : Set.Finite t) : ((finprod fun (i : α) => finprod fun (h : i ∈ s) => f i) * finprod fun (i : α) => finprod fun (h : i ∈ t \ s) => f i) = finprod fun (i : α) => finprod fun (h : i ∈ t) => f i

Given a finite set t and a subset s of t, the product of f i over i ∈ s times the product of f i over t \ s equals the product of f i over i ∈ t.

theorem finsum_mem_iUnion {α : Type u_1} {ι : Type u_3} {M : Type u_5} [AddCommMonoid M] {f : α → M} [Finite ι] {t : ι → Set α} (h : Pairwise (Disjoint on t)) (ht : ∀ (i : ι), Set.Finite (t i)) : (finsum fun (a : α) => finsum fun (h : a ∈ ⋃ (i : ι), t i) => f a) = finsum fun (i : ι) => finsum fun (a : α) => finsum fun (h : a ∈ t i) => f a

Given a family of pairwise disjoint finite sets t i indexed by a finite type, the sum of f a over the union ⋃ i, t i is equal to the sum over all indexes i of the sums of f a over a ∈ t i.

theorem finprod_mem_iUnion {α : Type u_1} {ι : Type u_3} {M : Type u_5} [CommMonoid M] {f : α → M} [Finite ι] {t : ι → Set α} (h : Pairwise (Disjoint on t)) (ht : ∀ (i : ι), Set.Finite (t i)) : (finprod fun (a : α) => finprod fun (h : a ∈ ⋃ (i : ι), t i) => f a) = finprod fun (i : ι) => finprod fun (a : α) => finprod fun (h : a ∈ t i) => f a

Given a family of pairwise disjoint finite sets t i indexed by a finite type, the product of f a over the union ⋃ i, t i is equal to the product over all indexes i of the products of f a over a ∈ t i.

theorem finsum_mem_biUnion {α : Type u_1} {ι : Type u_3} {M : Type u_5} [AddCommMonoid M] {f : α → M} {I : Set ι} {t : ι → Set α} (h : Set.PairwiseDisjoint I t) (hI : Set.Finite I) (ht : ∀ i ∈ I, Set.Finite (t i)) : (finsum fun (a : α) => finsum fun (h : a ∈ ⋃ x ∈ I, t x) => f a) = finsum fun (i : ι) => finsum fun (h : i ∈ I) => finsum fun (j : α) => finsum fun (h : j ∈ t i) => f j

Given a family of sets t : ι → Set α, a finite set I in the index type such that all sets t i, i ∈ I, are finite, if all t i, i ∈ I, are pairwise disjoint, then the sum of f a over a ∈ ⋃ i ∈ I, t i is equal to the sum over i ∈ I of the sums of f a over a ∈ t i.

theorem finprod_mem_biUnion {α : Type u_1} {ι : Type u_3} {M : Type u_5} [CommMonoid M] {f : α → M} {I : Set ι} {t : ι → Set α} (h : Set.PairwiseDisjoint I t) (hI : Set.Finite I) (ht : ∀ i ∈ I, Set.Finite (t i)) : (finprod fun (a : α) => finprod fun (h : a ∈ ⋃ x ∈ I, t x) => f a) = finprod fun (i : ι) => finprod fun (h : i ∈ I) => finprod fun (j : α) => finprod fun (h : j ∈ t i) => f j

Given a family of sets t : ι → Set α, a finite set I in the index type such that all sets t i, i ∈ I, are finite, if all t i, i ∈ I, are pairwise disjoint, then the product of f a over a ∈ ⋃ i ∈ I, t i is equal to the product over i ∈ I of the products of f a over a ∈ t i.

theorem finsum_mem_sUnion {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {t : Set (Set α)} (h : Set.PairwiseDisjoint t id) (ht₀ : Set.Finite t) (ht₁ : ∀ x ∈ t, Set.Finite x) : (finsum fun (a : α) => finsum fun (h : a ∈ ⋃₀ t) => f a) = finsum fun (s : Set α) => finsum fun (h : s ∈ t) => finsum fun (a : α) => finsum fun (h : a ∈ s) => f a

If t is a finite set of pairwise disjoint finite sets, then the sum of f a over a ∈ ⋃₀ t is the sum over s ∈ t of the sums of f a over a ∈ s.

theorem finprod_mem_sUnion {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {t : Set (Set α)} (h : Set.PairwiseDisjoint t id) (ht₀ : Set.Finite t) (ht₁ : ∀ x ∈ t, Set.Finite x) : (finprod fun (a : α) => finprod fun (h : a ∈ ⋃₀ t) => f a) = finprod fun (s : Set α) => finprod fun (h : s ∈ t) => finprod fun (a : α) => finprod fun (h : a ∈ s) => f a

If t is a finite set of pairwise disjoint finite sets, then the product of f a over a ∈ ⋃₀ t is the product over s ∈ t of the products of f a over a ∈ s.

theorem add_finsum_cond_ne {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} (a : α) (hf : Set.Finite (Function.support f)) : (f a + finsum fun (i : α) => finsum fun (x : i ≠ a) => f i) = finsum fun (i : α) => f i

theorem mul_finprod_cond_ne {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} (a : α) (hf : Set.Finite (Function.mulSupport f)) : (f a * finprod fun (i : α) => finprod fun (x : i ≠ a) => f i) = finprod fun (i : α) => f i

theorem finsum_mem_comm {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {s : Set α} {t : Set β} (f : α → β → M) (hs : Set.Finite s) (ht : Set.Finite t) : (finsum fun (i : α) => finsum fun (h : i ∈ s) => finsum fun (j : β) => finsum fun (h : j ∈ t) => f i j) = finsum fun (j : β) => finsum fun (h : j ∈ t) => finsum fun (i : α) => finsum fun (h : i ∈ s) => f i j

If s : Set α and t : Set β are finite sets, then summing over s commutes with summing over t.

theorem finprod_mem_comm {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] {s : Set α} {t : Set β} (f : α → β → M) (hs : Set.Finite s) (ht : Set.Finite t) : (finprod fun (i : α) => finprod fun (h : i ∈ s) => finprod fun (j : β) => finprod fun (h : j ∈ t) => f i j) = finprod fun (j : β) => finprod fun (h : j ∈ t) => finprod fun (i : α) => finprod fun (h : i ∈ s) => f i j

If s : Set α and t : Set β are finite sets, then taking the product over s commutes with taking the product over t.

theorem finsum_mem_induction {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s : Set α} (p : M → Prop) (hp₀ : p 0) (hp₁ : ∀ (x y : M), p x → p y → p (x + y)) (hp₂ : ∀ x ∈ s, p (f x)) : p (finsum fun (i : α) => finsum fun (h : i ∈ s) => f i)

To prove a property of a finite sum, it suffices to prove that the property is additive and holds on summands.

theorem finprod_mem_induction {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s : Set α} (p : M → Prop) (hp₀ : p 1) (hp₁ : ∀ (x y : M), p x → p y → p (x * y)) (hp₂ : ∀ x ∈ s, p (f x)) : p (finprod fun (i : α) => finprod fun (h : i ∈ s) => f i)

To prove a property of a finite product, it suffices to prove that the property is multiplicative and holds on factors.

theorem finprod_cond_nonneg {α : Type u_1} {R : Type u_7} [OrderedCommSemiring R] {p : α → Prop} {f : α → R} (hf : ∀ (x : α), p x → 0 ≤ f x) : 0 ≤ finprod fun (x : α) => finprod fun (x_1 : p x) => f x

theorem single_le_finsum {α : Type u_1} {M : Type u_7} [OrderedAddCommMonoid M] (i : α) {f : α → M} (hf : Set.Finite (Function.support f)) (h : ∀ (j : α), 0 ≤ f j) : f i ≤ finsum fun (j : α) => f j

theorem single_le_finprod {α : Type u_1} {M : Type u_7} [OrderedCommMonoid M] (i : α) {f : α → M} (hf : Set.Finite (Function.mulSupport f)) (h : ∀ (j : α), 1 ≤ f j) : f i ≤ finprod fun (j : α) => f j

theorem finprod_eq_zero {α : Type u_1} {M₀ : Type u_7} [CommMonoidWithZero M₀] (f : α → M₀) (x : α) (hx : f x = 0) (hf : Set.Finite (Function.mulSupport f)) : (finprod fun (x : α) => f x) = 0

theorem finsum_sum_comm {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (s : Finset β) (f : α → β → M) (h : ∀ b ∈ s, Set.Finite (Function.support fun (a : α) => f a b)) : (finsum fun (a : α) => Finset.sum s fun (b : β) => f a b) = Finset.sum s fun (b : β) => finsum fun (a : α) => f a b

theorem finprod_prod_comm {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] (s : Finset β) (f : α → β → M) (h : ∀ b ∈ s, Set.Finite (Function.mulSupport fun (a : α) => f a b)) : (finprod fun (a : α) => Finset.prod s fun (b : β) => f a b) = Finset.prod s fun (b : β) => finprod fun (a : α) => f a b

theorem sum_finsum_comm {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (s : Finset α) (f : α → β → M) (h : ∀ a ∈ s, Set.Finite (Function.support (f a))) : (Finset.sum s fun (a : α) => finsum fun (b : β) => f a b) = finsum fun (b : β) => Finset.sum s fun (a : α) => f a b

theorem prod_finprod_comm {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] (s : Finset α) (f : α → β → M) (h : ∀ a ∈ s, Set.Finite (Function.mulSupport (f a))) : (Finset.prod s fun (a : α) => finprod fun (b : β) => f a b) = finprod fun (b : β) => Finset.prod s fun (a : α) => f a b

theorem mul_finsum {α : Type u_1} {R : Type u_7} [Semiring R] (f : α → R) (r : R) (h : Set.Finite (Function.support f)) : (r * finsum fun (a : α) => f a) = finsum fun (a : α) => r * f a

theorem finsum_mul {α : Type u_1} {R : Type u_7} [Semiring R] (f : α → R) (r : R) (h : Set.Finite (Function.support f)) : (finsum fun (a : α) => f a) * r = finsum fun (a : α) => f a * r

theorem Finset.support_of_fiberwise_sum_subset_image {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] [DecidableEq β] (s : Finset α) (f : α → M) (g : α → β) : (Function.support fun (b : β) => Finset.sum (Finset.filter (fun (a : α) => g a = b) s) f) ⊆ ↑(Finset.image g s)

theorem Finset.mulSupport_of_fiberwise_prod_subset_image {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] [DecidableEq β] (s : Finset α) (f : α → M) (g : α → β) : (Function.mulSupport fun (b : β) => Finset.prod (Finset.filter (fun (a : α) => g a = b) s) f) ⊆ ↑(Finset.image g s)

theorem finsum_mem_finset_product' {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] [DecidableEq α] [DecidableEq β] (s : Finset (α × β)) (f : α × β → M) : (finsum fun (ab : α × β) => finsum fun (x : ab ∈ s) => f ab) = finsum fun (a : α) => finsum fun (b : β) => finsum fun (x : b ∈ Finset.image Prod.snd (Finset.filter (fun (ab : α × β) => ab.1 = a) s)) => f (a, b)

Note that b ∈ (s.filter (fun ab => Prod.fst ab = a)).image Prod.snd iff (a, b) ∈ s so we can simplify the right hand side of this lemma. However the form stated here is more useful for iterating this lemma, e.g., if we have f : α × β × γ → M.

theorem finprod_mem_finset_product' {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] [DecidableEq α] [DecidableEq β] (s : Finset (α × β)) (f : α × β → M) : (finprod fun (ab : α × β) => finprod fun (x : ab ∈ s) => f ab) = finprod fun (a : α) => finprod fun (b : β) => finprod fun (x : b ∈ Finset.image Prod.snd (Finset.filter (fun (ab : α × β) => ab.1 = a) s)) => f (a, b)

Note that b ∈ (s.filter (fun ab => Prod.fst ab = a)).image Prod.snd iff (a, b) ∈ s so we can simplify the right hand side of this lemma. However the form stated here is more useful for iterating this lemma, e.g., if we have f : α × β × γ → M.

theorem finsum_mem_finset_product {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (s : Finset (α × β)) (f : α × β → M) : (finsum fun (ab : α × β) => finsum fun (x : ab ∈ s) => f ab) = finsum fun (a : α) => finsum fun (b : β) => finsum fun (x : (a, b) ∈ s) => f (a, b)

See also finsum_mem_finset_product'.

theorem finprod_mem_finset_product {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] (s : Finset (α × β)) (f : α × β → M) : (finprod fun (ab : α × β) => finprod fun (x : ab ∈ s) => f ab) = finprod fun (a : α) => finprod fun (b : β) => finprod fun (x : (a, b) ∈ s) => f (a, b)

See also finprod_mem_finset_product'.

theorem finsum_mem_finset_product₃ {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {γ : Type u_7} (s : Finset (α × β × γ)) (f : α × β × γ → M) : (finsum fun (abc : α × β × γ) => finsum fun (x : abc ∈ s) => f abc) = finsum fun (a : α) => finsum fun (b : β) => finsum fun (c : γ) => finsum fun (x : (a, b, c) ∈ s) => f (a, b, c)

theorem finprod_mem_finset_product₃ {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] {γ : Type u_7} (s : Finset (α × β × γ)) (f : α × β × γ → M) : (finprod fun (abc : α × β × γ) => finprod fun (x : abc ∈ s) => f abc) = finprod fun (a : α) => finprod fun (b : β) => finprod fun (c : γ) => finprod fun (x : (a, b, c) ∈ s) => f (a, b, c)

theorem finsum_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (f : α × β → M) (hf : Set.Finite (Function.support f)) : (finsum fun (ab : α × β) => f ab) = finsum fun (a : α) => finsum fun (b : β) => f (a, b)

theorem finprod_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] (f : α × β → M) (hf : Set.Finite (Function.mulSupport f)) : (finprod fun (ab : α × β) => f ab) = finprod fun (a : α) => finprod fun (b : β) => f (a, b)

theorem finsum_curry₃ {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {γ : Type u_7} (f : α × β × γ → M) (h : Set.Finite (Function.support f)) : (finsum fun (abc : α × β × γ) => f abc) = finsum fun (a : α) => finsum fun (b : β) => finsum fun (c : γ) => f (a, b, c)

theorem finprod_curry₃ {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] {γ : Type u_7} (f : α × β × γ → M) (h : Set.Finite (Function.mulSupport f)) : (finprod fun (abc : α × β × γ) => f abc) = finprod fun (a : α) => finprod fun (b : β) => finprod fun (c : γ) => f (a, b, c)

theorem finsum_dmem {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (f : (a : α) → a ∈ s → M) : (finsum fun (a : α) => finsum fun (h : a ∈ s) => f a h) = finsum fun (a : α) => finsum fun (x : a ∈ s) => if h' : a ∈ s then f a h' else 0

theorem finprod_dmem {α : Type u_1} {M : Type u_5} [CommMonoid M] {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (f : (a : α) → a ∈ s → M) : (finprod fun (a : α) => finprod fun (h : a ∈ s) => f a h) = finprod fun (a : α) => finprod fun (x : a ∈ s) => if h' : a ∈ s then f a h' else 1

theorem finsum_emb_domain' {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : α → β} (hf : Function.Injective f) [DecidablePred fun (x : β) => x ∈ Set.range f] (g : α → M) : (finsum fun (b : β) => if h : b ∈ Set.range f then g (Classical.choose h) else 0) = finsum fun (a : α) => g a

theorem finprod_emb_domain' {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] {f : α → β} (hf : Function.Injective f) [DecidablePred fun (x : β) => x ∈ Set.range f] (g : α → M) : (finprod fun (b : β) => if h : b ∈ Set.range f then g (Classical.choose h) else 1) = finprod fun (a : α) => g a

theorem finsum_emb_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (f : α ↪ β) [DecidablePred fun (x : β) => x ∈ Set.range ⇑f] (g : α → M) : (finsum fun (b : β) => if h : b ∈ Set.range ⇑f then g (Classical.choose h) else 0) = finsum fun (a : α) => g a

theorem finprod_emb_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [CommMonoid M] (f : α ↪ β) [DecidablePred fun (x : β) => x ∈ Set.range ⇑f] (g : α → M) : (finprod fun (b : β) => if h : b ∈ Set.range ⇑f then g (Classical.choose h) else 1) = finprod fun (a : α) => g a