Lemmas about Multiset.sum
and Multiset.prod
requiring extra algebra imports #
@[simp]
theorem
Multiset.prod_eq_zero
{M₀ : Type u_3}
[CommMonoidWithZero M₀]
{s : Multiset M₀}
(h : 0 ∈ s)
:
@[simp]
theorem
Multiset.prod_eq_zero_iff
{M₀ : Type u_3}
[CommMonoidWithZero M₀]
[NoZeroDivisors M₀]
[Nontrivial M₀]
{s : Multiset M₀}
:
theorem
Multiset.prod_ne_zero
{M₀ : Type u_3}
[CommMonoidWithZero M₀]
[NoZeroDivisors M₀]
[Nontrivial M₀]
{s : Multiset M₀}
(h : 0 ∉ s)
:
theorem
Commute.multiset_sum_right
{R : Type u_4}
[NonUnitalNonAssocSemiring R]
(s : Multiset R)
(a : R)
(h : ∀ b ∈ s, Commute a b)
:
theorem
Commute.multiset_sum_left
{R : Type u_4}
[NonUnitalNonAssocSemiring R]
(s : Multiset R)
(b : R)
(h : ∀ a ∈ s, Commute a b)
: