Multiset.noncommFold_coe
theorem Multiset.noncommFold_coe :
∀ {α : Type u_3} (op : α → α → α) [assoc : Std.Associative op] (l : List α)
(comm : {x | x ∈ ↑l}.Pairwise fun x y => op x y = op y x) (a : α),
Multiset.noncommFold op (↑l) comm a = List.foldr op a l
This theorem establishes the equality between the noncommutative fold of a multiset and the right-to-left fold of a list. More specifically, for any type `α`, any binary operation `op` on `α` that is associative, any list `l` of `α`, and any element `a` of `α`, if the operation `op` is commutative for all distinct pairs of elements in the list `l`, then the noncommutative fold of a multiset obtained from `l` using the operation `op`, starting with `a`, is equal to the right-to-left fold of the list `l` using the operation `op`, starting with `a`.
More concisely: For any commutative, associative binary operation `op` on type `α`, any list `l` of `α` with distinct elements, and any `a` in `α`, the noncommutative multiset fold of `a` and `l` using `op` equals the right-to-left list fold of `l` using `op` starting with `a`.
|
Finset.noncommProd_mul_distrib
theorem Finset.noncommProd_mul_distrib :
∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] {s : Finset α} (f g : α → β)
(comm_ff : (↑s).Pairwise fun x y => Commute (f x) (f y)) (comm_gg : (↑s).Pairwise fun x y => Commute (g x) (g y))
(comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)),
s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
The theorem `Finset.noncommProd_mul_distrib` is a non-commutative version of the product distribution property over a finite set. Given a monoid `β`, a finite set `s` of elements from another type `α`, and two functions `f` and `g` mapping elements of `α` to elements of `β`, it states that if pairwise elements under these functions commute with each other, then the non-commutative product of `s` under the function `f * g` is equal to the product of the non-commutative product of `s` under `f` and the non-commutative product of `s` under `g`. Here, two elements `a` and `b` are said to commute if `a * b = b * a`, and a relation holds pairwise if it is valid for all distinct pairs of elements.
More concisely: If `β` is a monoid, `s` is a finite set of commuting elements from `α`, and `f` and `g` are functions mapping `α` to `β`, then `(∏ x ∈ s :: f x) * (∏ y ∈ s :: g y) = ∏ x ∈ s :: (f x * g x)`.
|
Multiset.noncommFoldr_coe
theorem Multiset.noncommFoldr_coe :
∀ {α : Type u_3} {β : Type u_4} (f : α → β → β) (l : List α)
(comm : {x | x ∈ ↑l}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)) (b : β),
Multiset.noncommFoldr f (↑l) comm b = List.foldr f b l
This theorem states that for any types `α` and `β`, a function `f` of type `α → β → β`, a list `l` of type `List α`, a property `comm` stating that for each pair of distinct elements `x` and `y` in the multiset coerced from `l`, the function `f` commutes for each `b : β` (i.e., `f x (f y b) = f y (f x b)`), and a `b : β`, the non-commutative fold of `f` over the multiset coerced from `l` with the `comm` property starting with `b` is equal to the right-to-left fold of `f` over the list `l` starting with `b`.
In simpler terms, it connects two ways of combining elements in a list: one in an unordered way (with a proof that the process is independent of the order), and one in a specific order from right to left. It states that these two ways produce the same result when the function used is commutative for all pairs of elements in the multiset.
More concisely: For any commutative function `f : α → β → β`, list `l : List α`, and `b : β`, the non-commutative fold of `f` over the multiset of `l` equals the right-to-left fold of `f` over `l` starting with `b`.
|
Multiset.noncommSum_coe
theorem Multiset.noncommSum_coe :
∀ {α : Type u_3} [inst : AddMonoid α] (l : List α) (comm : {x | x ∈ ↑l}.Pairwise AddCommute),
(↑l).noncommSum comm = l.sum
This theorem states that for any list `l` of elements of a certain type `α` under an additive monoid structure, if the pairwise addition of all distinct elements in this list is commutative (i.e., the order of addition does not affect the result), then the non-commutative sum of the elements in this list (seen as a multiset and computed by `Multiset.noncommSum`) is equal to the regular sum of the elements in the list (computed by `List.sum`). In this sense, this theorem establishes a connection between the sum of elements in a list and the non-commutative sum of elements in a multiset when the addition operation is commutative.
More concisely: If `l` is a list of commutative additive monoid elements, then `Multiset.noncommSum l` equals `List.sum l`.
|
Multiset.noncommProd_coe
theorem Multiset.noncommProd_coe :
∀ {α : Type u_3} [inst : Monoid α] (l : List α) (comm : {x | x ∈ ↑l}.Pairwise Commute),
(↑l).noncommProd comm = l.prod
This theorem, `Multiset.noncommProd_coe`, states that for any type `α` that forms a monoid, given a list `l` of elements of `α` such that each pair of distinct elements in `l` commute (i.e., their multiplication is commutative), when `l` is considered as a multiset and its elements' non-commutative product is calculated using `Multiset.noncommProd`, the result is equal to the usual product of the list `l` computed using `List.prod`. In simpler terms, even if we treat our list as a multiset and consider a non-commutative product, as long as all elements commute, we get the same result as the standard list product.
More concisely: For any commutative monoid type `α` and list `l` of `α` such that each pair of distinct elements commutes, `Multiset.noncommProd l = List.prod l`.
|
Finset.noncommProd_lemma
theorem Finset.noncommProd_lemma :
∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] (s : Finset α) (f : α → β),
((↑s).Pairwise fun a b => Commute (f a) (f b)) → {x | x ∈ Multiset.map f s.val}.Pairwise Commute
The theorem `Finset.noncommProd_lemma` states that for any types α and β where β is a Monoid, given a finite set of elements of type α, `s`, and a function `f` mapping elements of α to β, if for every pair of distinct elements in set s, `f` applied to these elements commute (i.e., their order doesn't affect the result), then it is also true that Commute holds pairwise for the set of elements obtained by mapping `f` over the multiset derived from `s`. In other words, the theorem ensures that commutativity is preserved when applying the function `f` to all elements of the set `s`.
More concisely: If `f : α -> β` is a function between types `α` and `β` where `β` is a monoid, and `s : Finset α` is a finite set such that `f (a1) * f (a2) = f (a2) * f (a1)` for all distinct `a1, a2 in s`, then `f''(s)` is a commutative multiset in `β`, where `f'' : Finset α -> Finset β` is the function that maps each set to the multiset of images under `f`.
|
Mathlib.Data.Finset.NoncommProd._auxLemma.2
theorem Mathlib.Data.Finset.NoncommProd._auxLemma.2 : ∀ {α : Type u_1} {a : α} {l : List α}, (a ∈ ↑l) = (a ∈ l) := by
sorry
This theorem, `Mathlib.Data.Finset.NoncommProd._auxLemma.2`, states that for any type `α` and any element `a` of this type, as well as any list `l` of elements of type `α`, the condition of `a` being in the set representation (`↑l`) of the list `l` is equivalent to `a` being in the list `l` itself. In other words, an element is in a list if and only if it is in the set derived from that list.
More concisely: For any type `α` and list `l` of elements from `α`, the set representation `{x : α | x ∈ l}` of `l` equals `l` itself.
|
Finset.noncommProd_union_of_disjoint
theorem Finset.noncommProd_union_of_disjoint :
∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] [inst_1 : DecidableEq α] {s t : Finset α},
Disjoint s t →
∀ (f : α → β) (comm : {x | x ∈ s ∪ t}.Pairwise fun a b => Commute (f a) (f b)),
(s ∪ t).noncommProd f comm = s.noncommProd f ⋯ * t.noncommProd f ⋯
This theorem, `Finset.noncommProd_union_of_disjoint`, is a non-commutative version of the `Finset.prod_union` theorem. It states that for every two disjoint finite sets `s` and `t` of a type `α`, with a function `f` mapping `α` to a monoid `β`, if every pair of elements `(a, b)` in the union of `s` and `t` satisfies the `Commute` property, i.e., `f(a) * f(b) = f(b) * f(a)`, then the non-commutative product of the union of `s` and `t` under `f` is equal to the product of the non-commutative product of `s` under `f` and the non-commutative product of `t` under `f`. The `DecidableEq` instance for `α` is used to support the union operation on the finite sets.
More concisely: If two disjoint finite sets `s` and `t` of a type `α` with a monoid structure on `α` via a function `f` satisfy `f(a) * f(b) = f(b) * f(a)` for all `a ∈ s` and `b ∈ t`, then `∏(s ∪ t) ≈ ∏s ⊗ ∏t` under `f`.
|
Finset.noncommSum_add_distrib
theorem Finset.noncommSum_add_distrib :
∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] {s : Finset α} (f g : α → β)
(comm_ff : (↑s).Pairwise fun x y => AddCommute (f x) (f y))
(comm_gg : (↑s).Pairwise fun x y => AddCommute (g x) (g y))
(comm_gf : (↑s).Pairwise fun x y => AddCommute (g x) (f y)),
s.noncommSum (f + g) ⋯ = s.noncommSum f comm_ff + s.noncommSum g comm_gg
The theorem `Finset.noncommSum_add_distrib` is a non-commutative variation of the distributive property of sum over addition in a finite set. It states that for any two functions `f` and `g` from a type `α` to an additive monoid `β`, if the values of `f`, `g`, and `g` and `f` pairwise commute for all distinct elements in a finite set `s` (meaning `f(x) + f(y) = f(y) + f(x)`, `g(x) + g(y) = g(y) + g(x)`, and `g(x) + f(y) = f(y) + g(x)` for all `x ≠ y` in `s`), then the non-commutative sum of `f + g` over `s` is equal to the non-commutative sum of `f` over `s` plus the non-commutative sum of `g` over `s`.
More concisely: If functions `f` and `g` from type `α` to an additive monoid `β` commute pairwise on distinct elements of a finite set `s`, then the non-commutative sum of `f + g` over `s` equals the non-commutative sum of `f` over `s` plus the non-commutative sum of `g` over `s`.
|
Finset.noncommSum_lemma
theorem Finset.noncommSum_lemma :
∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] (s : Finset α) (f : α → β),
((↑s).Pairwise fun a b => AddCommute (f a) (f b)) → {x | x ∈ Multiset.map f s.val}.Pairwise AddCommute
This theorem, `Finset.noncommSum_lemma`, states that for any type `α` and `β`, given `β` is an additive monoid and provided a finite set `s` of type `α` and a function `f` mapping elements from type `α` to `β`, if the function `f` applied to any two distinct elements of the set `s` satisfies the additive commutativity property (i.e., `f a + f b = f b + f a`), then the same additive commutativity property holds for any two distinct elements in the multiset obtained by applying the function `f` to each element in the multiset equivalent to set `s`. In other words, the pairwise commutativity under addition of the images under `f` of elements in `s` is preserved when considering `s` as a multiset rather than a set.
More concisely: If `f : α → β` is a function mapping a finite set `s : Finset α` to an additive monoid `β`, and `f` satisfies `f a + f b = f b + f a` for all distinct `a, b ∈ s`, then the same commutativity property holds for any distinct `a, b` in the multiset obtained from `s` under `f`.
|
Finset.noncommSum_union_of_disjoint
theorem Finset.noncommSum_union_of_disjoint :
∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] [inst_1 : DecidableEq α] {s t : Finset α},
Disjoint s t →
∀ (f : α → β) (comm : {x | x ∈ s ∪ t}.Pairwise fun a b => AddCommute (f a) (f b)),
(s ∪ t).noncommSum f comm = s.noncommSum f ⋯ + t.noncommSum f ⋯
This theorem, `Finset.noncommSum_union_of_disjoint`, states a non-commutative version of summing over the union of two sets. Specifically, for any types `α` and `β`, where `β` is an additive monoid and `α` has decidable equality, and given two disjoint finite sets `s` and `t` of type `α`, if a function `f` from `α` to `β` satisfies the condition that for every pair of distinct elements `a` and `b` in the union of `s` and `t`, `f(a)` and `f(b)` commute with respect to addition, then the non-commutative sum of `f` over the union of `s` and `t` is equal to the sum of the non-commutative sum of `f` over `s` and the non-commutative sum of `f` over `t`. In other words, even though addition may not be commutative in `β`, we can still "distribute" the sum over the union of two disjoint sets.
More concisely: If `α` is a type with decidable equality, `β` is an additive monoid, and `s` and `t` are disjoint finite subsets of `α`, then for any function `f : α → β` such that `f(a)` and `f(b)` commute for all distinct `a ∈ s ∪ t`, we have `∑(x ∈ s ∪ t) f x = ∑(x ∈ s) f x + ∑(x ∈ t) f x`.
|