Theorems · Theorem · group theory
Finset.prod_eq_multiset_prod
∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (s : Finset ι) (f : ι → M),
∏ x ∈ s, f x = (Multiset.map f s.val).prod- Cited by
- 7 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Quot.sound
- Assumes
- CommMonoid
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
- Finset.prodstatement · cited by 2,356
- CommMonoidstatement and proof · cited by 2,264
- Multiset.mapstatement · cited by 876
- Multiset.prodstatement · cited by 528
- Finset.valstatement · cited by 438
Cited by7
Results whose statement or proof uses this declaration.
- Algebra.norm_eq_prod_embeddings_genproof · cited by 1
- Multiset.toFinset_prod_dvd_prodproof · cited by 1
- Associates.finsetProd_mkproof · cited by 1
- AlgebraicClosure.toSplittingField_coeffproof · cited by 1
- Polynomial.exists_finset_of_splitsproof · cited by 0
- Ideal.IsPrime.prod_mem_iff_exists_memproof · cited by 0
- MvPolynomial.prod_X_add_C_coeffproof · cited by 0