Multiset.prod_replicate
theorem Multiset.prod_replicate :
∀ {α : Type u_2} [inst : CommMonoid α] (n : ℕ) (a : α), (Multiset.replicate n a).prod = a ^ n
The theorem `Multiset.prod_replicate` states that for any type `α` which has a commutative monoid structure, any natural number `n`, and any element 'a' of type `α`, the product of the multiset obtained by replicating 'a' 'n' times (`a` being replicated `n` times forms a multiset, and we take the product of all elements in this multiset) is equal to 'a' raised to the power of 'n'. In mathematical terms, if we denote the multiset replication operation as a function, we can write this as: $\prod(\text{replicate}(n, a)) = a^n$.
More concisely: The theorem asserts that for any commutative monoid type `α`, natural number `n`, and element `a` of `α`, the product of `n` replicas of `a` equals `a` raised to the power of `n`.
|
Multiset.prod_add
theorem Multiset.prod_add : ∀ {α : Type u_2} [inst : CommMonoid α] (s t : Multiset α), (s + t).prod = s.prod * t.prod
The theorem `Multiset.prod_add` states that for any given type `α` that has a Commutative Monoid structure, the product of the multiset addition (concatenation) of two multisets `s` and `t` is equal to the product of the individual multisets `s` and `t`. Specifically, if we have two multisets `s` and `t`, the product of the multiset `s + t` (which represents the multiset formed by adding `t` to `s`) is the same as the product of the multiset `s` multiplied by the product of the multiset `t`. This is analogous to the distributive property in algebra where the multiplication of a sum is equal to the sum of the products.
More concisely: For any commutative monoid type `α`, the product of the multiset formed by adding two multisets `s` and `t` equals the product of `s` and the product of `t`.
|
Multiset.sum_map_add
theorem Multiset.sum_map_add :
∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] {m : Multiset ι} {f g : ι → α},
(Multiset.map (fun i => f i + g i) m).sum = (Multiset.map f m).sum + (Multiset.map g m).sum
The theorem `Multiset.sum_map_add` states that for any multiset `m` of a certain type `ι` and any two functions `f` and `g` from `ι` to a type `α` which has an additive commutative monoid structure, the sum of the multiset obtained by mapping each element of `m` to the sum of applying `f` and `g` to it is equal to the sum of adding the sum of the multiset obtained by mapping `f` on `m` and the sum of the multiset obtained by mapping `g` on `m`. Essentially, this theorem asserts the distributive property of addition over the map operation on multisets.
More concisely: For any additive commutative monoid type `α` and multiset `m` of type `ι`, the sum of the multiset obtained by mapping each element of `m` to the sum of `f` and `g` is equal to the sum of the multiset obtained by mapping `f` and then adding, and the sum of the multiset obtained by mapping `g` and then adding, where `f` and `g` are functions from `ι` to `α`.
|
Multiset.prod_dvd_prod_of_le
theorem Multiset.prod_dvd_prod_of_le :
∀ {α : Type u_2} [inst : CommMonoid α] {s t : Multiset α}, s ≤ t → s.prod ∣ t.prod
This theorem states that for any type `α` that has a structure of a commutative monoid, given two multisets `s` and `t` of type `α`, if `s` is a subset of (or equal to) `t`, then the product of elements in `s` divides the product of elements in `t`. In mathematical notation, this can be represented as: if $s \leq t$, then $\prod s | \prod t$.
More concisely: If `α` is a commutative monoid type and `s` is a subset of `t`, then $\prod s | \prod t$.
|
Multiset.sum_eq_zero
theorem Multiset.sum_eq_zero :
∀ {α : Type u_2} [inst : AddCommMonoid α] {s : Multiset α}, (∀ x ∈ s, x = 0) → s.sum = 0
This theorem states that for any type `α` in the context of an additive commutative monoid, and any multiset `s` of that type `α`, if all elements `x` in the multiset `s` are equal to zero, then the sum of the multiset `s` is also zero. In more mathematical terms, if our set is such that $\forall x \in s, x = 0$, then $\Sigma_{x \in s} x = 0$. This theorem essentially proves the intuitive fact that the sum of a collection of zeroes is zero, but in the general setting of an additive commutative monoid.
More concisely: In an additive commutative monoid, the sum of any multiset of zeroes is zero.
|
Multiset.sum_hom
theorem Multiset.sum_hom :
∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] (s : Multiset α) {F : Type u_5}
[inst_2 : FunLike F α β] [inst_3 : AddMonoidHomClass F α β] (f : F), (Multiset.map (⇑f) s).sum = f s.sum
The theorem `Multiset.sum_hom` establishes that for all types `α` and `β` where both `α` and `β` are equipped with a commutative additive monoid structure, and for a multiset `s` of type `α`, for all types `F` which are function-like from `α` to `β` and are also a homomorphism between the additive monoids of `α` and `β`, the sum of the multiset obtained by mapping a function `f` of type `F` over `s` is equal to the value of function `f` applied to the sum of multiset `s`. This means that the process of summing elements in a multiset commutes with the operation of mapping a homomorphism over the multiset.
More concisely: For all commutative additive monoids `α` and `β`, and for any homomorphism `F` from `α` to `β` and multiset `s` over `α`, the sum of `F` applied to the multiset `s` equals `F` applied to the sum of `s`.
|
Multiset.prod_cons
theorem Multiset.prod_cons :
∀ {α : Type u_2} [inst : CommMonoid α] (a : α) (s : Multiset α), (a ::ₘ s).prod = a * s.prod
The theorem `Multiset.prod_cons` states that for any type `α` that is a commutative monoid, and for any element `a` of that type and any multiset `s` of elements of the same type, the product of the multiset formed by adding `a` to the front of `s` is equal to `a` times the product of `s`. In mathematical terms, it says that if `s` is a multiset of elements of a commutative monoid, then the product of `a` and `s` (denoted `a * prod s`) is the same as the product of the multiset obtained by adding `a` to `s`.
More concisely: For any commutative monoid type `α` and element `a` of `α`, the product of `a` and the multiset `s` is equal to the product of the multiset obtained by adding `a` to the front of `s`. In other words, `a * prod s = a * s`.
|
Multiset.prod_hom
theorem Multiset.prod_hom :
∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] (s : Multiset α) {F : Type u_5}
[inst_2 : FunLike F α β] [inst_3 : MonoidHomClass F α β] (f : F), (Multiset.map (⇑f) s).prod = f s.prod
This theorem, `Multiset.prod_hom`, states that for any types `α` and `β` with commutative monoid structures, a multiset `s` of type `α`, a function type `F` such that it behaves like a function from `α` to `β` (indicated by `FunLike F α β`), and a function `f` of type `F` which is also a monoid homomorphism (indicated by `MonoidHomClass F α β`), the product of the multiset obtained by mapping `f` over `s` is equal to the result of applying `f` to the product of `s`. In other words, the function `f` preserves the product operation while being applied to each element of the multiset or to the entire product of the multiset, demonstrating its homomorphic property.
More concisely: For any commutative monoids `α` and `β`, given a multiset `s` of type `α`, a function `F` that behaves like a function from `α` to `β` and is a monoid homomorphism `F: MonoidHomClass α β`, the product of `s` mapped under `F` equals the product of `F` applied to the product of `s`.
|
map_multiset_sum
theorem map_multiset_sum :
∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {F : Type u_5}
[inst_2 : FunLike F α β] [inst_3 : AddMonoidHomClass F α β] (f : F) (s : Multiset α),
f s.sum = (Multiset.map (⇑f) s).sum
The theorem `map_multiset_sum` states that for any type `α` and `β`, which both have a structure of a commutative additive monoid, for any function-like `F` from `α` to `β` that is also a homomorphism with respect to the additive monoid structure, and for any multiset `s` of elements of type `α`, the result of applying the function `f` to the sum of the multiset `s` is equal to the sum of the multiset obtained by mapping `f` over `s`.
In other words, the function `f` commutes with the sum operation on multisets, and therefore can be interchanged with it. This is an instance of a more general property often encountered in mathematics, where a map preserves a certain operation (in this case, addition), which is expressed in the language of category theory as the map being a homomorphism.
More concisely: For any commutative additive monoid homomorphism F between types α and β, and any multiset s of elements from α, the application of F to the sum of s is equal to the sum of the images of s under F.
|
MonoidHom.map_multiset_prod
theorem MonoidHom.map_multiset_prod :
∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] (f : α →* β) (s : Multiset α),
f s.prod = (Multiset.map (⇑f) s).prod
The theorem `MonoidHom.map_multiset_prod` states that for any two types `α` and `β` with commutative monoid structures, a monoid homomorphism `f` from `α` to `β`, and a multiset `s` of type `α`, applying `f` to the product of the multiset `s` (i.e., `f (Multiset.prod s)`) is equal to the product of the multiset obtained by mapping `f` over `s` (i.e., `Multiset.prod (Multiset.map (⇑f) s)`). In other words, this theorem asserts that a monoid homomorphism preserves the product operation on multisets, and this behavior is invariant to the order of operations due to the commutative property.
More concisely: For any commutative monoids `α` and `β`, a monoid homomorphism `f` from `α` to `β` preserves the product operation on multisets, i.e., `f (Multiset.prod s) = Multiset.prod (Multiset.map (f) s)`.
|
Multiset.sum_add
theorem Multiset.sum_add : ∀ {α : Type u_2} [inst : AddCommMonoid α] (s t : Multiset α), (s + t).sum = s.sum + t.sum
This theorem states that for any type `α` that has an additive commutative monoid structure, and for any two multisets `s` and `t` of this type, the sum of the multiset obtained by adding `s` and `t` is equal to the sum of `s` plus the sum of `t`. In other words, it asserts the distributive property of sum over the addition of multisets.
More concisely: For any additive commutative monoid type `α`, the sum of the multiset obtained by adding two multisets `s` and `t` of type `α` is equal to the multiset obtained by adding their individual sums.
|
Multiset.sum_zero
theorem Multiset.sum_zero : ∀ {α : Type u_2} [inst : AddCommMonoid α], Multiset.sum 0 = 0
The theorem `Multiset.sum_zero` states that for any type `α` that has an additive commutative monoid structure, the sum of an empty multiset in `α` is the identity element of the addition operation in the monoid, which is zero. In other words, when we sum up all elements in an empty multiset, the result is always zero, no matter what the type `α` is, as long as it is an additive commutative monoid.
More concisely: For any additive commutative monoid type `α`, the sum of an empty multiset in `α` equals its additive identity (zero).
|
Multiset.sum_singleton
theorem Multiset.sum_singleton : ∀ {α : Type u_2} [inst : AddCommMonoid α] (a : α), {a}.sum = a
This theorem states that for any type `α` that has a commutative additive monoid structure, the sum of a multiset containing a single element `a` of type `α` is equal to `a` itself. In other words, if you have a multiset with just one element `a`, when you sum up all elements in the multiset using the defined sum operation for the type `α`, you get `a` back.
More concisely: For any commutative additive monoid type `α`, the sum of a multiset containing a single element `a` equals `a`.
|
map_multiset_prod
theorem map_multiset_prod :
∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {F : Type u_5}
[inst_2 : FunLike F α β] [inst_3 : MonoidHomClass F α β] (f : F) (s : Multiset α),
f s.prod = (Multiset.map (⇑f) s).prod
The theorem `map_multiset_prod` states that for any two types `α` and `β` with commutative monoid structures, any `FunLike` object `F` from `α` to `β` that also obeys `MonoidHomClass` (making `F` a monoid homomorphism), a function `f` of type `F`, and a multiset `s` of type `α`, the result of applying `f` to the product of the multiset `s` is equal to the product of the multiset obtained by mapping `f` over `s`. This can be interpreted as the homomorphism `f` preserving the product operation while transforming elements from `α` to `β`.
More concisely: For any commutative monoids types `α` and `β`, any `FunLike` monoid homomorphism `F` from `α` to `β`, and any multiset `s` of `α`, the application of `F` to the product of `s` is equal to the product of the image of `s` under `F`.
|
AddMonoidHom.map_multiset_sum
theorem AddMonoidHom.map_multiset_sum :
∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] (f : α →+ β) (s : Multiset α),
f s.sum = (Multiset.map (⇑f) s).sum
This theorem states that for any two types `α` and `β` that have an additive commutative monoid structure, any homomorphism `f` from `α` to `β`, and any multiset `s` of type `α`, the result of applying `f` to the sum of `s` is equal to the sum of the multiset obtained by mapping `f` over `s`. In mathematical terms, it says that the sum operation commutes with the map operation under the homomorphism `f`, that is, $f(\sum s) = \sum (f \mapsto s)$, where $\sum$ denotes the sum operation on multisets and $\mapsto$ denotes the map operation on multisets.
More concisely: For any additive commutative monoids types `α` and `β`, any homomorphism `f` from `α` to `β`, and any multiset `s` of type `α`, the application of `f` to the sum of `s` is equal to the sum of the image of `s` under `f`. In mathematical notation: $f(\sum s) = \sum (f(x) \mid x \in s)$.
|
Multiset.prod_map_mul
theorem Multiset.prod_map_mul :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] {m : Multiset ι} {f g : ι → α},
(Multiset.map (fun i => f i * g i) m).prod = (Multiset.map f m).prod * (Multiset.map g m).prod
This theorem, `Multiset.prod_map_mul`, states that for any type `ι`, type `α` with a commutative monoid structure, multiset `m` of type `ι`, and functions `f` and `g` mapping from `ι` to `α`, the product of the multiset obtained by mapping each element in `m` to the product of `f i` and `g i` (where `i` is an element in `m`) equals the product of the multiset obtained by mapping each element in `m` via `f` multiplied by the product of the multiset obtained by mapping each element in `m` via `g`. In mathematical terms, we can express this as $\prod_{i \in m} (f(i)g(i)) = (\prod_{i \in m} f(i))(\prod_{i \in m} g(i))$.
More concisely: The product of multisets obtained by mapping each element in a multiset to the product of two functions is equal to the product of the multisets obtained by mapping each element to each function separately, for any commutative monoid type and commutative monoid structure on its functions.
|
Multiset.sum_replicate
theorem Multiset.sum_replicate :
∀ {α : Type u_2} [inst : AddCommMonoid α] (n : ℕ) (a : α), (Multiset.replicate n a).sum = n • a
The theorem `Multiset.sum_replicate` states that for any type `α` that has a commutative additive monoid structure, and for any natural number `n` and any element `a` of type `α`, the sum of a multiset created by replicating `a` `n` times is equal to `n` times `a`. This means that if you create a multiset with `n` copies of `a` and then sum them all up, you get the same result as if you just multiplied `a` by `n`. The symbol `•` denotes scalar multiplication in this context.
More concisely: For any commutative additive monoid type `α` and natural number `n`, the sum of `n` copies of an element `a` in a multiset equals `n • a`.
|
Multiset.prod_eq_one
theorem Multiset.prod_eq_one : ∀ {α : Type u_2} [inst : CommMonoid α] {s : Multiset α}, (∀ x ∈ s, x = 1) → s.prod = 1
This theorem states that for any type `α` that forms a commutative monoid, if we have a multiset `s` of elements of type `α`, and every element `x` in `s` equals to `1`, then the product of all elements in `s` will also be `1`. In other words, if all elements of a multiset in a commutative monoid are `1`, then the product over the entire multiset is `1`. The commutative monoid structure ensures that the operation is associative and has an identity element, in this case `1`.
More concisely: If `α` is a commutative monoid and `s` is a multiset of elements from `α` all equal to `1`, then the product of elements in `s` is equal to `1`.
|
Multiset.sum_cons
theorem Multiset.sum_cons :
∀ {α : Type u_2} [inst : AddCommMonoid α] (a : α) (s : Multiset α), (a ::ₘ s).sum = a + s.sum
The theorem `Multiset.sum_cons` states that for any type `α` that has the structure of a commutative additive monoid, any element `a` of type `α`, and any multiset `s` of elements of type `α`, the sum of the multiset obtained by adding `a` to `s` is equal to the sum of `a` and the sum of `s`. In other words, if you add an element to a multiset, the sum of the new multiset is just the sum of the old multiset plus the added element. This is a property related to the distributive law in the additive monoid.
More concisely: For any commutative additive monoid type `α` and element `a` of `α`, the sum of a multiset `s` and `a` equals the sum of `s` and `a`.
|
Multiset.prod_singleton
theorem Multiset.prod_singleton : ∀ {α : Type u_2} [inst : CommMonoid α] (a : α), {a}.prod = a
This theorem states that for any type `α` that has a commutative monoid structure, the product of a multiset that contains only one element `a` of type `α` (denoted by `Multiset.prod {a}`) is equal to the element `a` itself. In other words, the product of a singleton multiset `{a}` is `a` itself, where `*` is the multiplication operation defined in the commutitive monoid structure on `α`.
More concisely: For any commutative monoid type `α`, the product of a singleton multiset `{a}` equals the element `a` itself, i.e., `Multiset.prod {a} = a`.
|
Multiset.prod_zero
theorem Multiset.prod_zero : ∀ {α : Type u_2} [inst : CommMonoid α], Multiset.prod 0 = 1
This theorem states that the product of an empty multiset equals the identity element of a commutative monoid. Given any type `α` with a commutative monoid structure, when we apply the `Multiset.prod` function to an empty multiset (denoted by `0`), we get the multiplicative identity of that monoid, which is `1`.
More concisely: For any commutative monoid type `α`, the product of an empty multiset over `α` equals the monoid's identity element.
|