Mathlib Map

Theorems · Theorem · combinatorics

Multiset.prod_eq_prod_coe

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommMonoid α] (m : Multiset α), m.prod = ∏ x, x.fst
Defined in
Mathlib.Data.Multiset.Fintype
Cited by
1 results in Mathlib
Foundations
Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
DecidableEqCommMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Polynomial.isIntegral_coeff_of_factors · cited by 1Polynomial.isIntegral_coe…Finset.univ · cited by 3473Finset.univMultiset · cited by 2627MultisetFinset.prod · cited by 2356Finset.prodCommMonoid · cited by 2264CommMonoidMultiset.map · cited by 876Multiset.mapMultiset.prod · cited by 528Multiset.prodFinset.val · cited by 438Finset.valMultiset.count · cited by 302Multiset.countMultiset.ToType · cited by 30Multiset.ToTypeMultiset.map_univ_coe · cited by 3Multiset.map_univ_coeMultiset.prod_eq_prod_coeCITED BYCITES

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.