Theorems · Theorem · group theory
Multiset.toFinset_prod_dvd_prod
∀ {M : Type u_3} [inst : DecidableEq M] [inst_1 : CommMonoid M] (S : Multiset M), S.toFinset.prod id ∣ S.prod- Cited by
- 1 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Multisetstatement and proof · cited by 2,627
- Finset.prodstatement · cited by 2,356
- CommMonoidstatement and proof · cited by 2,264
- Multiset.prodstatement and proof · cited by 528
- Multiset.map_congrproof · cited by 232
- Multiset.toFinsetstatement and proof · cited by 230
- Multiset.dedupproof · cited by 59
- Multiset.map_id'proof · cited by 35
- Multiset.prod_dvd_prod_of_leproof · cited by 9
- Multiset.dedup_leproof · cited by 9
- Finset.prod_eq_multiset_prodproof · cited by 7
Cited by1
Results whose statement or proof uses this declaration.
- Nat.prod_primeFactors_dvdproof · cited by 9