mathlib3 documentation

algebra.big_operators.multiset.lemmas

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
theorem multiset.dvd_prod {α : Type u_2} [comm_monoid α] {s : multiset α} {a : α} :
a ∈ s → a ∣ s.prod
source
theorem multiset.sum_eq_zero_iff {α : Type u_2} [canonically_ordered_add_monoid α] {m : multiset α} :
m.sum = 0 ↔ ∀ (x : α), x ∈ m → x = 0
source
theorem multiset.prod_eq_one_iff {α : Type u_2} [canonically_ordered_monoid α] {m : multiset α} :
m.prod = 1 ↔ ∀ (x : α), x ∈ m → x = 1
source
theorem commute.multiset_sum_right {α : Type u_2} [non_unital_non_assoc_semiring α] (s : multiset α) (a : α) (h : ∀ (b : α), b ∈ s → commute a b) :
commute a s.sum
source
theorem commute.multiset_sum_left {α : Type u_2} [non_unital_non_assoc_semiring α] (s : multiset α) (b : α) (h : ∀ (a : α), a ∈ s → commute a b) :
commute s.sum b