Multiset.prod_eq_zero_iff
theorem Multiset.prod_eq_zero_iff :
∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NoZeroDivisors α] [inst_2 : Nontrivial α] {s : Multiset α},
s.prod = 0 ↔ 0 ∈ s
This theorem states that for any multiset `s` of elements from a type `α`, where `α` is a commutative monoid with zero, has no zero divisors, and is nontrivial, the product of the elements in `s` equals zero if and only if zero is an element of `s`. In other words, the product of a multiset is zero if and only if the multiset contains zero, under the given conditions for the type of the elements.
More concisely: For a commutative monoid with zero and no zero divisors and nontrivial elements, a multiset of such elements has product equal to zero if and only if it contains the zero element.
|
Multiset.dvd_sum
theorem Multiset.dvd_sum :
∀ {α : Type u_1} [inst : NonUnitalSemiring α] {s : Multiset α} {a : α}, (∀ x ∈ s, a ∣ x) → a ∣ s.sum
This theorem states that for any type `α` equipped with the structure of a non-unital semiring, and for any multiset `s` of elements of `α` and any element `a` of `α`, if `a` divides every element in `s`, then `a` also divides the sum of all elements in `s`. In other words, if each item in a multiset is divisible by a particular number, then the sum of the multiset is also divisible by that number.
More concisely: If `α` is a semiring and `a` divides every element in a multiset `s` over `α`, then `a` divides the sum of `s`.
|
Multiset.dvd_prod
theorem Multiset.dvd_prod : ∀ {α : Type u_1} [inst : CommMonoid α] {s : Multiset α} {a : α}, a ∈ s → a ∣ s.prod := by
sorry
The theorem `Multiset.dvd_prod` states that for any type `α` which has a Commutative Monoid structure, for any multiset `s` of type `α`, and for any element `a` of type `α`, if `a` is an element of `s`, then `a` divides the product of all elements in `s`. Here, the product of a multiset is defined as the product of all elements in the multiset, similar to how mathematical product works. For example, the product of the multiset `{a, b, c}` is `a * b * c`.
More concisely: For any commutative monoid type `α` and multiset `s` of `α`, if `a` is an element of `s`, then `a` divides the product of all elements in `s`.
|