Theorems · Theorem · group theory
Multiset.prod_dvd_prod_of_le
∀ {M : Type u_5} [inst : CommMonoid M] {s t : Multiset M}, s ≤ t → s.prod ∣ t.prod- Cited by
- 9 results in Mathlib
- Foundations
- Depth 25 from the axioms · 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.
- Multisetstatement and proof · cited by 2,627
- CommMonoidstatement and proof · cited by 2,264
- Multiset.prodstatement and proof · cited by 528
- ExistsAddOfLE.exists_add_of_leproof · cited by 42
- Multiset.prod_addproof · cited by 18
Cited by9
Results whose statement or proof uses this declaration.
- UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactorsproof · cited by 11
- UniqueFactorizationMonoid.radical_dvd_selfproof · cited by 7
- Finset.prod_dvd_prod_of_subsetproof · cited by 6
- Polynomial.count_map_rootsproof · cited by 2
- Polynomial.Splits.dvd_of_roots_le_rootsproof · cited by 1
- Multiset.toFinset_prod_dvd_prodproof · cited by 1
- Nat.divisors_filter_squarefreeproof · cited by 1
- Polynomial.normalizedFactors_cyclotomic_cardproof · cited by 0
- Multiset.prod_X_sub_C_dvd_iff_le_rootsproof · cited by 0