finset

In this file we provide some elementary results for summations

theorem Finset.sum_rotate {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} [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

theorem Finset.sum_3_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} [AddCommMonoid β] {s : Finset α} {t : Finset γ} {u : Finset ζ} {f : α → γ → ζ → β} : ∑ x ∈ s, ∑ y ∈ t, ∑ z ∈ u, f x y z = ∑ z ∈ u, ∑ y ∈ t, ∑ x ∈ s, f x y z

theorem Finset.sum_4_rotate {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {ε : Type u_5} [AddCommMonoid β] {s : Finset α} {t : Finset γ} {u : Finset ζ} {v : Finset ε} {f : α → γ → ζ → ε → β} : ∑ x ∈ s, ∑ y ∈ t, ∑ z ∈ u, ∑ w ∈ v, f x y z w = ∑ w ∈ v, ∑ x ∈ s, ∑ y ∈ t, ∑ z ∈ u, f x y z w

theorem Finset.sum_sum_comm_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {ε : Type u_5} [AddCommMonoid β] {s : Finset α} {t : Finset γ} {u : Finset ζ} {v : Finset ε} {f : α → γ → ζ → ε → β} : ∑ x ∈ s, ∑ y ∈ t, ∑ z ∈ u, ∑ w ∈ v, f x y z w = ∑ x ∈ s, ∑ y ∈ t, ∑ w ∈ v, ∑ z ∈ u, f x y z w

theorem Finset.sum_sum_sum {β : Type u_1} {α : Type u_2} {γ : Type u_3} {ζ : Type u_4} [AddCommMonoid β] {s : Finset γ} {t : Finset α} {g : Finset ζ} {f : γ → α → ζ → β} : ∑ x ∈ s, ∑ y ∈ t, ∑ z ∈ g, f x y z = ∑ z ∈ g, ∑ x ∈ s, ∑ y ∈ t, f x y z

theorem Finset.sum_4_swap_2 {β : Type u_1} {α : Type u_2} {γ : Type u_3} {ζ : Type u_4} {ε : Type u_5} [AddCommMonoid β] {s : Finset γ} {t : Finset α} {u : Finset ζ} {v : Finset ε} {f : γ → α → ζ → ε → β} : ∑ x ∈ s, ∑ y ∈ t, ∑ z ∈ u, ∑ w ∈ v, f x y z w = ∑ z ∈ u, ∑ w ∈ v, ∑ x ∈ s, ∑ y ∈ t, f x y z w

theorem Finset.sum_5_rotate {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {ε : Type u_5} {κ : Type u_6} [AddCommMonoid β] {s : Finset α} {t : Finset γ} {u : Finset ζ} {v : Finset ε} {k : Finset κ} {f : α → γ → ζ → ε → κ → β} : ∑ x ∈ s, ∑ y ∈ t, ∑ z ∈ u, ∑ w ∈ v, ∑ vz ∈ k, f x y z w vz = ∑ vz ∈ k, ∑ x ∈ s, ∑ y ∈ t, ∑ z ∈ u, ∑ w ∈ v, f x y z w vz

theorem Forall.rotate {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {p : α → β → γ → Prop} : (∀ (x : α) (y : β) (z : γ), p x y z) ↔ ∀ (z : γ) (x : α) (y : β), p x y z

theorem forall_forall_comm {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {ζ : Sort u_4} {p : α → β → γ → ζ → Prop} : (∀ (x : α) (y : β) (z : γ) (w : ζ), p x y z w) ↔ ∀ (x : α) (z : γ) (y : β) (w : ζ), p x y z w

theorem Finset.sum_product_univ {β : Type u_1} {α : Type u_2} {γ : Type u_3} [AddCommMonoid β] [Fintype α] [Fintype γ] {f : γ × α → β} : ∑ x : γ × α, f x = ∑ x : γ, ∑ y : α, f (x, y)