Theorems · Theorem · group theory
Finset.sum_comm
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β},
∑ x ∈ s, ∑ y ∈ t, f x y = ∑ y ∈ t, ∑ x ∈ s, f x y- Cited by
- 66 results in Mathlib
- Foundations
- Depth 76 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.
Cites4
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
- Finset.sum_comm'proof · cited by 2
Cited by66
Results whose statement or proof uses this declaration.
- Matrix.det_mulproof · cited by 51
- Matrix.dotProduct_mulVecproof · cited by 19
- LinearMap.toMatrix₂_compl₁₂proof · cited by 7
- Finsupp.sum_commproof · cited by 7
- LinearMap.toMatrix₂'_compl₁₂proof · cited by 6
- TensorProduct.sum_tmul_eq_zero_of_vanishesTriviallyproof · cited by 4
- gaussSum_mul_gaussSum_eq_cardproof · cited by 4
- dotProduct_assocproof · cited by 3
- InnerProductSpace.canonicalCovariantTensor_eq_sumproof · cited by 3
- Algebra.traceMatrix_of_matrix_vecMulproof · cited by 2
- Finset.expect_sum_commproof · cited by 2
- Finset.sum_card_inter_leproof · cited by 2