Product and sums indexed by finite sets in sigma types.

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.

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.

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.

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

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)

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)

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

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

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)

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)

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

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

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'.

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'

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.

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

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)

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)

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.

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

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 Finsets depend on the outer variable.

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 Finsets depend on the outer variable.

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

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

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.

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

@[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