Documentation

Mathlib.Algebra.BigOperators.Multiset.Lemmas

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

theorem Multiset.dvd_prod {α : Type u_1} [inst : CommMonoid α] {s : Multiset α} {a : α} :
a sa Multiset.prod s
theorem Multiset.sum_eq_zero_iff {α : Type u_1} [inst : CanonicallyOrderedAddMonoid α] {m : Multiset α} :
Multiset.sum m = 0 ∀ (x : α), x mx = 0
theorem Multiset.prod_eq_one_iff {α : Type u_1} [inst : CanonicallyOrderedMonoid α] {m : Multiset α} :
Multiset.prod m = 1 ∀ (x : α), x mx = 1
@[simp]
theorem CanonicallyOrderedCommSemiring.multiset_prod_pos {R : Type u_1} [inst : CanonicallyOrderedCommSemiring R] [inst : Nontrivial R] {m : Multiset R} :
0 < Multiset.prod m ∀ (x : R), x m0 < x
theorem Commute.multiset_sum_right {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (s : Multiset α) (a : α) (h : ∀ (b : α), b sCommute a b) :
theorem Commute.multiset_sum_left {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (s : Multiset α) (b : α) (h : ∀ (a : α), a sCommute a b) :