Associates.prod_mk
theorem Associates.prod_mk :
∀ {α : Type u_1} [inst : CommMonoid α] {p : Multiset α},
(Multiset.map Associates.mk p).prod = Associates.mk p.prod
The theorem `Associates.prod_mk` states that for any commutative monoid `α` and any multiset `p` of type `α`, the product of the multiset obtained by mapping the canonical quotient map `Associates.mk` over `p` is equal to the `Associates.mk` of the product of `p`. In other words, it asserts that the operation of taking the product of a multiset commutes with the operation of mapping `Associates.mk` over the elements of the multiset.
More concisely: For any commutative monoid `α` and multiset `p` of type `α`, the product of the multiset `p` mapped through `Associates.mk` is equal to `Associates.mk` of the product of `p`.
|
Prime.dvd_finset_prod_iff
theorem Prime.dvd_finset_prod_iff :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoidWithZero M] {S : Finset α} {p : M},
Prime p → ∀ (g : α → M), p ∣ S.prod g ↔ ∃ a ∈ S, p ∣ g a
The theorem `Prime.dvd_finset_prod_iff` states that for any commutative monoid with zero `M` and any finite set `S` of elements from a type `α`, if `p` is a prime element of `M`, then `p` divides the product of a function `g` applied to each element of `S`, if and only if there exists an element `a` in `S` such that `p` divides `g(a)`. In other words, a prime divides the product of a set if and only if it divides at least one element in the set.
More concisely: For a commutative monoid with zero M and a finite set S of elements from type α, a prime p of M divides the product of a function g applied to each element in S if and only if there exists an a in S such that p divides g(a).
|