Documentation

Mathlib.Algebra.BigOperators.Ring.Multiset

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

@[simp]
theorem Multiset.prod_map_neg {α : Type u_2} [CommMonoid α] [HasDistribNeg α] (s : Multiset α) :
(Multiset.map Neg.neg s).prod = (-1) ^ Multiset.card s * s.prod
theorem Multiset.prod_eq_zero {α : Type u_2} [CommMonoidWithZero α] {s : Multiset α} (h : 0 s) :
s.prod = 0
@[simp]
theorem Multiset.prod_eq_zero_iff {α : Type u_2} [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {s : Multiset α} :
s.prod = 0 0 s
theorem Multiset.prod_ne_zero {α : Type u_2} [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {s : Multiset α} (h : 0s) :
s.prod 0
theorem Multiset.sum_map_mul_left {ι : Type u_1} {α : Type u_2} [NonUnitalNonAssocSemiring α] {a : α} {s : Multiset ι} {f : ια} :
(Multiset.map (fun (i : ι) => a * f i) s).sum = a * (Multiset.map f s).sum
theorem Multiset.sum_map_mul_right {ι : Type u_1} {α : Type u_2} [NonUnitalNonAssocSemiring α] {a : α} {s : Multiset ι} {f : ια} :
(Multiset.map (fun (i : ι) => f i * a) s).sum = (Multiset.map f s).sum * a
theorem Multiset.dvd_sum {α : Type u_2} [NonUnitalSemiring α] {s : Multiset α} {a : α} :
(∀ xs, a x)a s.sum
theorem Multiset.prod_map_sum {α : Type u_2} [CommSemiring α] {s : Multiset (Multiset α)} :
(Multiset.map Multiset.sum s).prod = (Multiset.map Multiset.prod s.Sections).sum
theorem Multiset.prod_map_add {ι : Type u_1} {α : Type u_2} [CommSemiring α] {s : Multiset ι} {f : ια} {g : ια} :
(Multiset.map (fun (i : ι) => f i + g i) s).prod = (Multiset.map (fun (p : Multiset ι × Multiset ι) => (Multiset.map f p.1).prod * (Multiset.map g p.2).prod) s.antidiagonal).sum
theorem Commute.multiset_sum_right {α : Type u_2} [NonUnitalNonAssocSemiring α] (s : Multiset α) (a : α) (h : bs, Commute a b) :
Commute a s.sum
theorem Commute.multiset_sum_left {α : Type u_2} [NonUnitalNonAssocSemiring α] (s : Multiset α) (b : α) (h : as, Commute a b) :
Commute s.sum b