Theorems · Definition · group theory
Finset.prod
{ι : Type u_1} → {M : Type u_3} → [CommMonoid M] → Finset ι → (ι → M) → M∏ x ∈ s, f x is the product of f x as x ranges over the elements of the finite set s.
When the index type is a Fintype, the notation ∏ x, f x, is a shorthand for
∏ x ∈ Finset.univ, f x.
- Cited by
- 2,356 results in Mathlib
- Foundations
- Depth 13 from the axioms, rests on 87 definitions · uses propext, Quot.sound
- Assumes
- CommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- CommMonoidstatement and proof · cited by 2,264
- Multiset.mapproof · cited by 876
- Multiset.prodproof · cited by 528
- Finset.valproof · cited by 438
Cited by2,415
Results whose statement or proof uses this declaration.
- Finset.prod_congrstatement and proof · cited by 646
- Finsupp.prodproof · cited by 231
- HasProdproof · cited by 157
- Finset.prod_conststatement · cited by 154
- Finset.prod_insertstatement · cited by 109
- map_prodstatement · cited by 108
- Finset.prod_const_onestatement · cited by 100
- Multipliable.hasProdproof · cited by 88
- Finset.prod_singletonstatement · cited by 78
- Finset.prod_mapstatement and proof · cited by 75
- Finset.prod_applystatement · cited by 70
- Finset.prod_mul_distribstatement and proof · cited by 68
Showing the 200 most cited of 2,415.