Documentation

Mathlib.Algebra.BigOperators.Ring.Multiset

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

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