Theorems · Theorem · group theory
Finset.sum_product
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : 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'
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Finset.sumstatement · cited by 5,195
- SProd.sprodstatement and proof · cited by 1,750
- Finset.mem_productproof · cited by 48
- Finset.sum_finset_productproof · cited by 3
Cited by27
Results whose statement or proof uses this declaration.
- Finset.sum_product'proof · cited by 8
- Fintype.sum_prod_typeproof · cited by 6
- AddMonoidAlgebra.coeff_mul_antidiagproof · cited by 3
- summable_mul_of_summable_norm'proof · cited by 3
- Matrix.kroneckerMapBilinear_mul_mulproof · cited by 3
- Configuration.HasLines.lineCount_eq_pointCountproof · cited by 3
- Matrix.vec_vecMul_kronecker_of_commuteproof · cited by 2
- Chebyshev.sum_PrimePow_eq_sum_sum'proof · cited by 2
- Matrix.kronecker_mulVec_vec_of_commuteproof · cited by 2
- Algebra.trace_trace_of_basisproof · cited by 2
- Matrix.trace_kroneckerMapBilinearproof · cited by 2
- IncidenceAlgebra.prod_mul_prod'proof · cited by 2