# Product and sums indexed by finite sets in sigma types. #

source
theorem Finset.prod_sigma {α : Type u_3} {β : Type u_4} [CommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : Sigma σ → β) :
∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩

The product over a sigma type equals the product of the fiberwise products. For rewriting in the reverse direction, use `Finset.prod_sigma'`.

See also `Fintype.prod_sigma` for the product over the whole type.

source
theorem Finset.sum_sigma {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : Sigma σ → β) :
∑ x ∈ s.sigma t, f x = ∑ a ∈ s, ∑ s ∈ t a, f ⟨a, s⟩

The sum over a sigma type equals the sum of the fiberwise sums. For rewriting in the reverse direction, use `Finset.sum_sigma'`.

See also `Fintype.sum_sigma` for the sum over the whole type.

source
theorem Finset.prod_sigma' {α : Type u_3} {β : Type u_4} [CommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : (a : α) → σ a → β) :
∏ a ∈ s, ∏ s ∈ t a, f a s = ∏ x ∈ s.sigma t, f x.fst x.snd

The product over a sigma type equals the product of the fiberwise products. For rewriting in the reverse direction, use `Finset.prod_sigma`.

source
theorem Finset.sum_sigma' {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : (a : α) → σ a → β) :
∑ a ∈ s, ∑ s ∈ t a, f a s = ∑ x ∈ s.sigma t, f x.fst x.snd

The sum over a sigma type equals the sum of the fiberwise sums. For rewriting in the reverse direction, use `Finset.sum_sigma`

source
theorem Finset.prod_finset_product {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ × α → β} :
∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (c, a)
source
theorem Finset.sum_finset_product {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ × α → β} :
∑ p ∈ r, f p = ∑ c ∈ s, ∑ a ∈ t c, f (c, a)
source
theorem Finset.prod_finset_product' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ → α → β} :
∏ p ∈ r, f p.1 p.2 = ∏ c ∈ s, ∏ a ∈ t c, f c a
source
theorem Finset.sum_finset_product' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ → α → β} :
∑ p ∈ r, f p.1 p.2 = ∑ c ∈ s, ∑ a ∈ t c, f c a
source
theorem Finset.prod_finset_product_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α × γ → β} :
∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (a, c)
source
theorem Finset.sum_finset_product_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α × γ → β} :
∑ p ∈ r, f p = ∑ c ∈ s, ∑ a ∈ t c, f (a, c)
source
theorem Finset.prod_finset_product_right' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α → γ → β} :
∏ p ∈ r, f p.1 p.2 = ∏ c ∈ s, ∏ a ∈ t c, f a c
source
theorem Finset.sum_finset_product_right' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α → γ → β} :
∑ p ∈ r, f p.1 p.2 = ∑ c ∈ s, ∑ a ∈ t c, f a c
source
theorem Finset.prod_product {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (s : Finset γ) (t : Finset α) (f : γ × α → β) :
∏ x ∈ s ×ˢ t, f x = ∏ x ∈ s, ∏ y ∈ t, f (x, y)

The product over a product set equals the product of the fiberwise products. For rewriting in the reverse direction, use `Finset.prod_product'`.

source
theorem Finset.sum_product {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset γ) (t : Finset α) (f : γ × α → β) :
∑ x ∈ s ×ˢ t, f x = ∑ x ∈ s, ∑ y ∈ t, f (x, y)

The sum over a product set equals the sum of the fiberwise sums. For rewriting in the reverse direction, use `Finset.sum_product'`

source
theorem Finset.prod_product' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (s : Finset γ) (t : Finset α) (f : γ → α → β) :
∏ x ∈ s ×ˢ t, f x.1 x.2 = ∏ x ∈ s, ∏ y ∈ t, f x y

The product over a product set equals the product of the fiberwise products. For rewriting in the reverse direction, use `Finset.prod_product`.

source
theorem Finset.sum_product' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset γ) (t : Finset α) (f : γ → α → β) :
∑ x ∈ s ×ˢ t, f x.1 x.2 = ∑ x ∈ s, ∑ y ∈ t, f x y

The sum over a product set equals the sum of the fiberwise sums. For rewriting in the reverse direction, use `Finset.sum_product`

source
theorem Finset.prod_product_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (s : Finset γ) (t : Finset α) (f : γ × α → β) :
∏ x ∈ s ×ˢ t, f x = ∏ y ∈ t, ∏ x ∈ s, f (x, y)
source
theorem Finset.sum_product_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset γ) (t : Finset α) (f : γ × α → β) :
∑ x ∈ s ×ˢ t, f x = ∑ y ∈ t, ∑ x ∈ s, f (x, y)
source
theorem Finset.prod_product_right' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (s : Finset γ) (t : Finset α) (f : γ → α → β) :
∏ x ∈ s ×ˢ t, f x.1 x.2 = ∏ y ∈ t, ∏ x ∈ s, f x y

An uncurried version of `Finset.prod_product_right`.

source
theorem Finset.sum_product_right' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset γ) (t : Finset α) (f : γ → α → β) :
∑ x ∈ s ×ˢ t, f x.1 x.2 = ∑ y ∈ t, ∑ x ∈ s, f x y

An uncurried version of `Finset.sum_product_right`

source
theorem Finset.prod_comm' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset γ} {t : γ → Finset α} {t' : Finset α} {s' : α → Finset γ} (h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t') {f : γ → α → β} :
∏ x ∈ s, ∏ y ∈ t x, f x y = ∏ y ∈ t', ∏ x ∈ s' y, f x y

Generalization of `Finset.prod_comm` to the case when the inner `Finset`s depend on the outer variable.

source
theorem Finset.sum_comm' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset γ} {t : γ → Finset α} {t' : Finset α} {s' : α → Finset γ} (h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t') {f : γ → α → β} :
∑ x ∈ s, ∑ y ∈ t x, f x y = ∑ y ∈ t', ∑ x ∈ s' y, f x y

Generalization of `Finset.sum_comm` to the case when the inner `Finset`s depend on the outer variable.

source
theorem Finset.prod_comm {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β} :
∏ x ∈ s, ∏ y ∈ t, f x y = ∏ y ∈ t, ∏ x ∈ s, f x y
source
theorem Finset.sum_comm {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β} :
∑ x ∈ s, ∑ y ∈ t, f x y = ∑ y ∈ t, ∑ x ∈ s, f x y
source
theorem Finset.prod_comm_cycle {κ : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset γ} {t : Finset α} {u : Finset κ} {f : γ → α → κ → β} :
∏ x ∈ s, ∏ y ∈ t, ∏ z ∈ u, f x y z = ∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z

Cyclically permute 3 nested instances of `Finset.prod`.

source
theorem Finset.sum_comm_cycle {κ : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset γ} {t : Finset α} {u : Finset κ} {f : γ → α → κ → β} :
∑ x ∈ s, ∑ y ∈ t, ∑ z ∈ u, f x y z = ∑ z ∈ u, ∑ x ∈ s, ∑ y ∈ t, f x y z
source
@[simp]
theorem Finset.card_sigma {α : Type u_3} {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a)) :
(s.sigma t).card = ∑ a ∈ s, (t a).card