[GOAL]
α : Type u_1
inst✝ : CommMonoid α
s : Multiset α
a✝ : α
l : List α
a : α
h : a ∈ Quotient.mk (List.isSetoid α) l
⊢ a ∣ prod (Quotient.mk (List.isSetoid α) l)
[PROOFSTEP]
simpa using List.dvd_prod h
[GOAL]
α : Type u_1
inst✝ : CanonicallyOrderedMonoid α
m : Multiset α
l : List α
⊢ prod (Quotient.mk (List.isSetoid α) l) = 1 ↔ ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l → x = 1
[PROOFSTEP]
simpa using List.prod_eq_one_iff l
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : CanonicallyOrderedCommSemiring R
inst✝ : Nontrivial R
m : Multiset R
⊢ 0 < Multiset.prod m ↔ ∀ (x : R), x ∈ m → 0 < x
[PROOFSTEP]
rcases m with ⟨l⟩
[GOAL]
case mk
α : Type u_1
R : Type u_2
inst✝¹ : CanonicallyOrderedCommSemiring R
inst✝ : Nontrivial R
m : Multiset R
l : List R
⊢ 0 < Multiset.prod (Quot.mk Setoid.r l) ↔ ∀ (x : R), x ∈ Quot.mk Setoid.r l → 0 < x
[PROOFSTEP]
rw [Multiset.quot_mk_to_coe'', Multiset.coe_prod]
[GOAL]
case mk
α : Type u_1
R : Type u_2
inst✝¹ : CanonicallyOrderedCommSemiring R
inst✝ : Nontrivial R
m : Multiset R
l : List R
⊢ 0 < List.prod l ↔ ∀ (x : R), x ∈ ↑l → 0 < x
[PROOFSTEP]
exact CanonicallyOrderedCommSemiring.list_prod_pos
[GOAL]
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
s : Multiset α
a : α
h : ∀ (b : α), b ∈ s → Commute a b
⊢ Commute a (sum s)
[PROOFSTEP]
induction s using Quotient.inductionOn
[GOAL]
case h
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
s : Multiset α
a : α
a✝ : List α
h : ∀ (b : α), b ∈ Quotient.mk (List.isSetoid α) a✝ → Commute a b
⊢ Commute a (sum (Quotient.mk (List.isSetoid α) a✝))
[PROOFSTEP]
rw [quot_mk_to_coe, coe_sum]
[GOAL]
case h
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
s : Multiset α
a : α
a✝ : List α
h : ∀ (b : α), b ∈ Quotient.mk (List.isSetoid α) a✝ → Commute a b
⊢ Commute a (List.sum a✝)
[PROOFSTEP]
exact Commute.list_sum_right _ _ h
