Documentation

Mathlib.Algebra.BigOperators.Multiset.Lemmas

Lemmas about Multiset.sum and Multiset.prod requiring extra algebra imports #

theorem Multiset.dvd_prod {α : Type u_1} [CommMonoid α] {s : Multiset α} {a : α} :
a sa Multiset.prod s
@[simp]
theorem Multiset.prod_map_neg {α : Type u_1} [CommMonoid α] [HasDistribNeg α] (s : Multiset α) :
Multiset.prod (Multiset.map Neg.neg s) = (-1) ^ Multiset.card s * Multiset.prod s
theorem Multiset.prod_eq_zero {α : Type u_1} [CommMonoidWithZero α] {s : Multiset α} (h : 0 s) :
theorem Multiset.prod_ne_zero {α : Type u_1} [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {s : Multiset α} (h : 0s) :
theorem Multiset.sum_eq_zero_iff {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] {m : Multiset α} :
Multiset.sum m = 0 xm, x = 0
theorem Multiset.prod_eq_one_iff {α : Type u_1} [CanonicallyOrderedCommMonoid α] {m : Multiset α} :
Multiset.prod m = 1 xm, x = 1
theorem Multiset.dvd_sum {α : Type u_1} [NonUnitalSemiring α] {s : Multiset α} {a : α} :
(xs, a x)a Multiset.sum s
theorem Commute.multiset_sum_right {α : Type u_1} [NonUnitalNonAssocSemiring α] (s : Multiset α) (a : α) (h : bs, Commute a b) :
theorem Commute.multiset_sum_left {α : Type u_1} [NonUnitalNonAssocSemiring α] (s : Multiset α) (b : α) (h : as, Commute a b) :