Lemmas about Multiset.sum and Multiset.prod requiring extra algebra imports #
theorem
Multiset.dvd_prod
{α : Type u_1}
[inst : CommMonoid α]
{s : Multiset α}
{a : α}
:
a ∈ s → a ∣ Multiset.prod s
theorem
Multiset.sum_eq_zero_iff
{α : Type u_1}
[inst : CanonicallyOrderedAddMonoid α]
{m : Multiset α}
:
Multiset.sum m = 0 ↔ ∀ (x : α), x ∈ m → x = 0
theorem
Multiset.prod_eq_one_iff
{α : Type u_1}
[inst : CanonicallyOrderedMonoid α]
{m : Multiset α}
:
Multiset.prod m = 1 ↔ ∀ (x : α), x ∈ m → x = 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 ∈ m → 0 < x
theorem
Commute.multiset_sum_right
{α : Type u_1}
[inst : NonUnitalNonAssocSemiring α]
(s : Multiset α)
(a : α)
(h : ∀ (b : α), b ∈ s → Commute a b)
:
Commute a (Multiset.sum s)
theorem
Commute.multiset_sum_left
{α : Type u_1}
[inst : NonUnitalNonAssocSemiring α]
(s : Multiset α)
(b : α)
(h : ∀ (a : α), a ∈ s → Commute a b)
:
Commute (Multiset.sum s) b