Products (respectively, sums) over a finset or a multiset. #
The regular Finset.prod and Multiset.prod require [CommMonoid α].
Often, there are collections s : Finset α where [Monoid α] and we know,
in a dependent fashion, that for all the terms ∀ (x ∈ s) (y ∈ s), Commute x y.
This allows to still have a well-defined product over s.
Main definitions #
Finset.noncommProd, requiring a proof of commutativity of held termsMultiset.noncommProd, requiring a proof of commutativity of held terms
Implementation details #
While List.prod is defined via List.foldl, noncommProd is defined via
Multiset.foldr for neater proofs and definitions. By the commutativity assumption,
the two must be equal.
TODO: Tidy up this file by using the fact that the submonoid generated by commuting
elements is commutative and using the Finset.prod versions of lemmas to prove the noncommProd
version.
def
Multiset.noncommFoldr
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(s : Multiset α)
(comm : Set.Pairwise { x | x ∈ s } fun x y => ∀ (b : β), f x (f y b) = f y (f x b))
(b : β)
:
β
Fold of a s : Multiset α with f : α → β → β, given a proof that LeftCommutative f
on all elements x ∈ s.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Multiset.noncommFoldr_coe
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(l : List α)
(comm : Set.Pairwise { x | x ∈ ↑l } 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
@[simp]
theorem
Multiset.noncommFoldr_empty
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(h : Set.Pairwise { x | x ∈ 0 } fun x y => ∀ (b : β), f x (f y b) = f y (f x b))
(b : β)
:
Multiset.noncommFoldr f 0 h b = b
theorem
Multiset.noncommFoldr_cons
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(s : Multiset α)
(a : α)
(h : Set.Pairwise { x | x ∈ a ::ₘ s } fun x y => ∀ (b : β), f x (f y b) = f y (f x b))
(h' : Set.Pairwise { x | x ∈ s } fun x y => ∀ (b : β), f x (f y b) = f y (f x b))
(b : β)
:
Multiset.noncommFoldr f (a ::ₘ s) h b = f a (Multiset.noncommFoldr f s h' b)
theorem
Multiset.noncommFoldr_eq_foldr
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(s : Multiset α)
(h : LeftCommutative f)
(b : β)
:
Multiset.noncommFoldr f s (fun x x_1 y x_2 x_3 => h x y) b = Multiset.foldr f h b s
def
Multiset.noncommFold
{α : Type u_1}
(op : α → α → α)
[assoc : IsAssociative α op]
(s : Multiset α)
(comm : Set.Pairwise { x | x ∈ s } fun x y => op x y = op y x)
:
α → α
Fold of a s : Multiset α with an associative op : α → α → α, given a proofs that op
is commutative on all elements x ∈ s.
Equations
- Multiset.noncommFold op s comm = Multiset.noncommFoldr op s (_ : ∀ (x : α), x ∈ { x | x ∈ s } → ∀ (y : α), y ∈ { x | x ∈ s } → x ≠ y → ∀ (b : α), op x (op y b) = op y (op x b))
@[simp]
theorem
Multiset.noncommFold_coe
{α : Type u_1}
(op : α → α → α)
[assoc : IsAssociative α op]
(l : List α)
(comm : Set.Pairwise { x | x ∈ ↑l } fun x y => op x y = op y x)
(a : α)
:
Multiset.noncommFold op (↑l) comm a = List.foldr op a l
@[simp]
theorem
Multiset.noncommFold_empty
{α : Type u_1}
(op : α → α → α)
[assoc : IsAssociative α op]
(h : Set.Pairwise { x | x ∈ 0 } fun x y => op x y = op y x)
(a : α)
:
Multiset.noncommFold op 0 h a = a
theorem
Multiset.noncommFold_cons
{α : Type u_1}
(op : α → α → α)
[assoc : IsAssociative α op]
(s : Multiset α)
(a : α)
(h : Set.Pairwise { x | x ∈ a ::ₘ s } fun x y => op x y = op y x)
(h' : Set.Pairwise { x | x ∈ s } fun x y => op x y = op y x)
(x : α)
:
Multiset.noncommFold op (a ::ₘ s) h x = op a (Multiset.noncommFold op s h' x)
theorem
Multiset.noncommFold_eq_fold
{α : Type u_1}
(op : α → α → α)
[assoc : IsAssociative α op]
(s : Multiset α)
[inst : IsCommutative α op]
(a : α)
:
Multiset.noncommFold op s (_ : ∀ (x : α), x ∈ { x | x ∈ s } → ∀ (y : α), y ∈ { x | x ∈ s } → x ≠ y → op x y = op y x)
a = Multiset.fold op a s
def
Multiset.noncommSum
{α : Type u_1}
[inst : AddMonoid α]
(s : Multiset α)
(comm : Set.Pairwise { x | x ∈ s } AddCommute)
:
α
Sum of a s : Multiset α with [AddMonoid α], given a proof that + commutes
on all elements x ∈ s.
Equations
- Multiset.noncommSum s comm = Multiset.noncommFold (fun x x_1 => x + x_1) s comm 0
def
Multiset.noncommSum.proof_1
{α : Type u_1}
[inst : AddMonoid α]
:
IsAssociative α fun x x_1 => x + x_1
Equations
- (_ : IsAssociative α fun x x_1 => x + x_1) = (_ : IsAssociative α fun x x_1 => x + x_1)
def
Multiset.noncommProd
{α : Type u_1}
[inst : Monoid α]
(s : Multiset α)
(comm : Set.Pairwise { x | x ∈ s } Commute)
:
α
Product of a s : Multiset α with [Monoid α], given a proof that * commutes
on all elements x ∈ s.
Equations
- Multiset.noncommProd s comm = Multiset.noncommFold (fun x x_1 => x * x_1) s comm 1
@[simp]
theorem
Multiset.noncommSum_coe
{α : Type u_1}
[inst : AddMonoid α]
(l : List α)
(comm : Set.Pairwise { x | x ∈ ↑l } AddCommute)
:
Multiset.noncommSum (↑l) comm = List.sum l
@[simp]
theorem
Multiset.noncommProd_coe
{α : Type u_1}
[inst : Monoid α]
(l : List α)
(comm : Set.Pairwise { x | x ∈ ↑l } Commute)
:
Multiset.noncommProd (↑l) comm = List.prod l
@[simp]
theorem
Multiset.noncommSum_empty
{α : Type u_1}
[inst : AddMonoid α]
(h : Set.Pairwise { x | x ∈ 0 } AddCommute)
:
Multiset.noncommSum 0 h = 0
@[simp]
theorem
Multiset.noncommProd_empty
{α : Type u_1}
[inst : Monoid α]
(h : Set.Pairwise { x | x ∈ 0 } Commute)
:
Multiset.noncommProd 0 h = 1
@[simp]
theorem
Multiset.noncommSum_cons
{α : Type u_1}
[inst : AddMonoid α]
(s : Multiset α)
(a : α)
(comm : Set.Pairwise { x | x ∈ a ::ₘ s } AddCommute)
:
Multiset.noncommSum (a ::ₘ s) comm = a + Multiset.noncommSum s (_ : Set.Pairwise { x | x ∈ s } AddCommute)
@[simp]
theorem
Multiset.noncommProd_cons
{α : Type u_1}
[inst : Monoid α]
(s : Multiset α)
(a : α)
(comm : Set.Pairwise { x | x ∈ a ::ₘ s } Commute)
:
Multiset.noncommProd (a ::ₘ s) comm = a * Multiset.noncommProd s (_ : Set.Pairwise { x | x ∈ s } Commute)
theorem
Multiset.noncommSum_cons'
{α : Type u_1}
[inst : AddMonoid α]
(s : Multiset α)
(a : α)
(comm : Set.Pairwise { x | x ∈ a ::ₘ s } AddCommute)
:
Multiset.noncommSum (a ::ₘ s) comm = Multiset.noncommSum s (_ : Set.Pairwise { x | x ∈ s } AddCommute) + a
theorem
Multiset.noncommProd_cons'
{α : Type u_1}
[inst : Monoid α]
(s : Multiset α)
(a : α)
(comm : Set.Pairwise { x | x ∈ a ::ₘ s } Commute)
:
Multiset.noncommProd (a ::ₘ s) comm = Multiset.noncommProd s (_ : Set.Pairwise { x | x ∈ s } Commute) * a
theorem
Multiset.noncommSum_add
{α : Type u_1}
[inst : AddMonoid α]
(s : Multiset α)
(t : Multiset α)
(comm : Set.Pairwise { x | x ∈ s + t } AddCommute)
:
Multiset.noncommSum (s + t) comm = Multiset.noncommSum s (_ : Set.Pairwise { x | x ∈ s } AddCommute) + Multiset.noncommSum t (_ : Set.Pairwise { x | x ∈ t } AddCommute)
theorem
Multiset.noncommProd_add
{α : Type u_1}
[inst : Monoid α]
(s : Multiset α)
(t : Multiset α)
(comm : Set.Pairwise { x | x ∈ s + t } Commute)
:
Multiset.noncommProd (s + t) comm = Multiset.noncommProd s (_ : Set.Pairwise { x | x ∈ s } Commute) * Multiset.noncommProd t (_ : Set.Pairwise { x | x ∈ t } Commute)
theorem
Multiset.noncommSum_map_aux
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[inst : AddMonoid α]
[inst : AddMonoid β]
[inst : AddMonoidHomClass F α β]
(s : Multiset α)
(comm : Set.Pairwise { x | x ∈ s } AddCommute)
(f : F)
:
Set.Pairwise { x | x ∈ Multiset.map (↑f) s } AddCommute
theorem
Multiset.noncommProd_map_aux
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[inst : Monoid α]
[inst : Monoid β]
[inst : MonoidHomClass F α β]
(s : Multiset α)
(comm : Set.Pairwise { x | x ∈ s } Commute)
(f : F)
:
Set.Pairwise { x | x ∈ Multiset.map (↑f) s } Commute
theorem
Multiset.noncommSum_map
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[inst : AddMonoid α]
[inst : AddMonoid β]
[inst : AddMonoidHomClass F α β]
(s : Multiset α)
(comm : Set.Pairwise { x | x ∈ s } AddCommute)
(f : F)
:
↑f (Multiset.noncommSum s comm) = Multiset.noncommSum (Multiset.map (↑f) s) (_ : Set.Pairwise { x | x ∈ Multiset.map (↑f) s } AddCommute)
theorem
Multiset.noncommProd_map
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[inst : Monoid α]
[inst : Monoid β]
[inst : MonoidHomClass F α β]
(s : Multiset α)
(comm : Set.Pairwise { x | x ∈ s } Commute)
(f : F)
:
↑f (Multiset.noncommProd s comm) = Multiset.noncommProd (Multiset.map (↑f) s) (_ : Set.Pairwise { x | x ∈ Multiset.map (↑f) s } Commute)
theorem
Multiset.noncommSum_eq_card_nsmul
{α : Type u_1}
[inst : AddMonoid α]
(s : Multiset α)
(comm : Set.Pairwise { x | x ∈ s } AddCommute)
(m : α)
(h : ∀ (x : α), x ∈ s → x = m)
:
Multiset.noncommSum s comm = ↑Multiset.card s • m
theorem
Multiset.noncommProd_eq_pow_card
{α : Type u_1}
[inst : Monoid α]
(s : Multiset α)
(comm : Set.Pairwise { x | x ∈ s } Commute)
(m : α)
(h : ∀ (x : α), x ∈ s → x = m)
:
Multiset.noncommProd s comm = m ^ ↑Multiset.card s
theorem
Multiset.noncommSum_eq_sum
{α : Type u_1}
[inst : AddCommMonoid α]
(s : Multiset α)
:
Multiset.noncommSum s
(_ : ∀ (x : α), x ∈ { x | x ∈ s } → ∀ (x_2 : α), x_2 ∈ { x | x ∈ s } → x ≠ x_2 → AddCommute x x_2) = Multiset.sum s
theorem
Multiset.noncommProd_eq_prod
{α : Type u_1}
[inst : CommMonoid α]
(s : Multiset α)
:
Multiset.noncommProd s (_ : ∀ (x : α), x ∈ { x | x ∈ s } → ∀ (x_2 : α), x_2 ∈ { x | x ∈ s } → x ≠ x_2 → Commute x x_2) = Multiset.prod s
theorem
Multiset.noncommSum_addCommute
{α : Type u_1}
[inst : AddMonoid α]
(s : Multiset α)
(comm : Set.Pairwise { x | x ∈ s } AddCommute)
(y : α)
(h : ∀ (x : α), x ∈ s → AddCommute y x)
:
AddCommute y (Multiset.noncommSum s comm)
theorem
Multiset.noncommProd_commute
{α : Type u_1}
[inst : Monoid α]
(s : Multiset α)
(comm : Set.Pairwise { x | x ∈ s } Commute)
(y : α)
(h : ∀ (x : α), x ∈ s → Commute y x)
:
Commute y (Multiset.noncommProd s comm)
theorem
Finset.noncommSum_lemma
{α : Type u_1}
{β : Type u_2}
[inst : AddMonoid β]
(s : Finset α)
(f : α → β)
(comm : Set.Pairwise ↑s fun a b => AddCommute (f a) (f b))
:
Set.Pairwise { x | x ∈ Multiset.map f s.val } AddCommute
theorem
Finset.noncommProd_lemma
{α : Type u_1}
{β : Type u_2}
[inst : Monoid β]
(s : Finset α)
(f : α → β)
(comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b))
:
Set.Pairwise { x | x ∈ Multiset.map f s.val } Commute
Proof used in definition of `Finset.noncommProd
def
Finset.noncommSum
{α : Type u_1}
{β : Type u_2}
[inst : AddMonoid β]
(s : Finset α)
(f : α → β)
(comm : Set.Pairwise ↑s fun a b => AddCommute (f a) (f b))
:
β
Sum of a s : Finset α mapped with f : α → β with [AddMonoid β],
given a proof that + commutes on all elements f x for x ∈ s.
Equations
- Finset.noncommSum s f comm = Multiset.noncommSum (Multiset.map f s.val) (_ : Set.Pairwise { x | x ∈ Multiset.map f s.val } AddCommute)
def
Finset.noncommProd
{α : Type u_1}
{β : Type u_2}
[inst : Monoid β]
(s : Finset α)
(f : α → β)
(comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b))
:
β
Product of a s : Finset α mapped with f : α → β with [Monoid β],
given a proof that * commutes on all elements f x for x ∈ s.
Equations
- Finset.noncommProd s f comm = Multiset.noncommProd (Multiset.map f s.val) (_ : Set.Pairwise { x | x ∈ Multiset.map f s.val } Commute)
theorem
Finset.noncommSum_congr
{α : Type u_1}
{β : Type u_2}
[inst : AddMonoid β]
{s₁ : Finset α}
{s₂ : Finset α}
{f : α → β}
{g : α → β}
(h₁ : s₁ = s₂)
(h₂ : ∀ (x : α), x ∈ s₂ → f x = g x)
(comm : Set.Pairwise ↑s₁ fun a b => AddCommute (f a) (f b))
:
Finset.noncommSum s₁ f comm = Finset.noncommSum s₂ g (_ : ∀ (x : α), x ∈ ↑s₂ → ∀ (y : α), y ∈ ↑s₂ → x ≠ y → (fun a b => AddCommute (g a) (g b)) x y)
theorem
Finset.noncommProd_congr
{α : Type u_1}
{β : Type u_2}
[inst : Monoid β]
{s₁ : Finset α}
{s₂ : Finset α}
{f : α → β}
{g : α → β}
(h₁ : s₁ = s₂)
(h₂ : ∀ (x : α), x ∈ s₂ → f x = g x)
(comm : Set.Pairwise ↑s₁ fun a b => Commute (f a) (f b))
:
Finset.noncommProd s₁ f comm = Finset.noncommProd s₂ g (_ : ∀ (x : α), x ∈ ↑s₂ → ∀ (y : α), y ∈ ↑s₂ → x ≠ y → (fun a b => Commute (g a) (g b)) x y)
@[simp]
theorem
Finset.noncommSum_toFinset
{α : Type u_1}
{β : Type u_2}
[inst : AddMonoid β]
[inst : DecidableEq α]
(l : List α)
(f : α → β)
(comm : Set.Pairwise ↑(List.toFinset l) fun a b => AddCommute (f a) (f b))
(hl : List.Nodup l)
:
Finset.noncommSum (List.toFinset l) f comm = List.sum (List.map f l)
@[simp]
theorem
Finset.noncommProd_toFinset
{α : Type u_1}
{β : Type u_2}
[inst : Monoid β]
[inst : DecidableEq α]
(l : List α)
(f : α → β)
(comm : Set.Pairwise ↑(List.toFinset l) fun a b => Commute (f a) (f b))
(hl : List.Nodup l)
:
Finset.noncommProd (List.toFinset l) f comm = List.prod (List.map f l)
@[simp]
theorem
Finset.noncommSum_empty
{α : Type u_1}
{β : Type u_2}
[inst : AddMonoid β]
(f : α → β)
(h : Set.Pairwise ↑∅ fun a b => AddCommute (f a) (f b))
:
Finset.noncommSum ∅ f h = 0
@[simp]
theorem
Finset.noncommProd_empty
{α : Type u_1}
{β : Type u_2}
[inst : Monoid β]
(f : α → β)
(h : Set.Pairwise ↑∅ fun a b => Commute (f a) (f b))
:
Finset.noncommProd ∅ f h = 1
@[simp]
theorem
Finset.noncommSum_insert_of_not_mem
{α : Type u_1}
{β : Type u_2}
[inst : AddMonoid β]
[inst : DecidableEq α]
(s : Finset α)
(a : α)
(f : α → β)
(comm : Set.Pairwise ↑(insert a s) fun a b => AddCommute (f a) (f b))
(ha : ¬a ∈ s)
:
Finset.noncommSum (insert a s) f comm = f a + Finset.noncommSum s f (_ : Set.Pairwise ↑s fun a b => AddCommute (f a) (f b))
@[simp]
theorem
Finset.noncommProd_insert_of_not_mem
{α : Type u_1}
{β : Type u_2}
[inst : Monoid β]
[inst : DecidableEq α]
(s : Finset α)
(a : α)
(f : α → β)
(comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b))
(ha : ¬a ∈ s)
:
Finset.noncommProd (insert a s) f comm = f a * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b))
theorem
Finset.noncommSum_insert_of_not_mem'
{α : Type u_1}
{β : Type u_2}
[inst : AddMonoid β]
[inst : DecidableEq α]
(s : Finset α)
(a : α)
(f : α → β)
(comm : Set.Pairwise ↑(insert a s) fun a b => AddCommute (f a) (f b))
(ha : ¬a ∈ s)
:
Finset.noncommSum (insert a s) f comm = Finset.noncommSum s f (_ : Set.Pairwise ↑s fun a b => AddCommute (f a) (f b)) + f a
theorem
Finset.noncommProd_insert_of_not_mem'
{α : Type u_1}
{β : Type u_2}
[inst : Monoid β]
[inst : DecidableEq α]
(s : Finset α)
(a : α)
(f : α → β)
(comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b))
(ha : ¬a ∈ s)
:
Finset.noncommProd (insert a s) f comm = Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) * f a
@[simp]
theorem
Finset.noncommSum_singleton
{α : Type u_2}
{β : Type u_1}
[inst : AddMonoid β]
(a : α)
(f : α → β)
:
Finset.noncommSum {a} f (_ : Set.Pairwise ↑{a} fun a b => AddCommute (f a) (f b)) = f a
@[simp]
theorem
Finset.noncommProd_singleton
{α : Type u_2}
{β : Type u_1}
[inst : Monoid β]
(a : α)
(f : α → β)
:
Finset.noncommProd {a} f (_ : Set.Pairwise ↑{a} fun a b => Commute (f a) (f b)) = f a
theorem
Finset.noncommSum_map
{F : Type u_1}
{α : Type u_4}
{β : Type u_2}
{γ : Type u_3}
[inst : AddMonoid β]
[inst : AddMonoid γ]
[inst : AddMonoidHomClass F β γ]
(s : Finset α)
(f : α → β)
(comm : Set.Pairwise ↑s fun a b => AddCommute (f a) (f b))
(g : F)
:
↑g (Finset.noncommSum s f comm) = Finset.noncommSum s (fun i => ↑g (f i))
(_ : ∀ (x : α), x ∈ ↑s → ∀ (y : α), y ∈ ↑s → x ≠ y → AddCommute (↑g (f x)) (↑g (f y)))
theorem
Finset.noncommProd_map
{F : Type u_1}
{α : Type u_4}
{β : Type u_2}
{γ : Type u_3}
[inst : Monoid β]
[inst : Monoid γ]
[inst : MonoidHomClass F β γ]
(s : Finset α)
(f : α → β)
(comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b))
(g : F)
:
↑g (Finset.noncommProd s f comm) = Finset.noncommProd s (fun i => ↑g (f i))
(_ : ∀ (x : α), x ∈ ↑s → ∀ (y : α), y ∈ ↑s → x ≠ y → Commute (↑g (f x)) (↑g (f y)))
theorem
Finset.noncommSum_eq_card_nsmul
{α : Type u_1}
{β : Type u_2}
[inst : AddMonoid β]
(s : Finset α)
(f : α → β)
(comm : Set.Pairwise ↑s fun a b => AddCommute (f a) (f b))
(m : β)
(h : ∀ (x : α), x ∈ s → f x = m)
:
Finset.noncommSum s f comm = Finset.card s • m
theorem
Finset.noncommProd_eq_pow_card
{α : Type u_1}
{β : Type u_2}
[inst : Monoid β]
(s : Finset α)
(f : α → β)
(comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b))
(m : β)
(h : ∀ (x : α), x ∈ s → f x = m)
:
Finset.noncommProd s f comm = m ^ Finset.card s
theorem
Finset.noncommSum_addCommute
{α : Type u_1}
{β : Type u_2}
[inst : AddMonoid β]
(s : Finset α)
(f : α → β)
(comm : Set.Pairwise ↑s fun a b => AddCommute (f a) (f b))
(y : β)
(h : ∀ (x : α), x ∈ s → AddCommute y (f x))
:
AddCommute y (Finset.noncommSum s f comm)
theorem
Finset.noncommProd_commute
{α : Type u_1}
{β : Type u_2}
[inst : Monoid β]
(s : Finset α)
(f : α → β)
(comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b))
(y : β)
(h : ∀ (x : α), x ∈ s → Commute y (f x))
:
Commute y (Finset.noncommProd s f comm)
theorem
Finset.noncommSum_eq_sum
{α : Type u_2}
{β : Type u_1}
[inst : AddCommMonoid β]
(s : Finset α)
(f : α → β)
:
Finset.noncommSum s f (_ : ∀ (x : α), x ∈ ↑s → ∀ (x_2 : α), x_2 ∈ ↑s → x ≠ x_2 → AddCommute (f x) (f x_2)) = Finset.sum s f
theorem
Finset.noncommProd_eq_prod
{α : Type u_2}
{β : Type u_1}
[inst : CommMonoid β]
(s : Finset α)
(f : α → β)
:
Finset.noncommProd s f (_ : ∀ (x : α), x ∈ ↑s → ∀ (x_2 : α), x_2 ∈ ↑s → x ≠ x_2 → Commute (f x) (f x_2)) = Finset.prod s f
theorem
Finset.noncommSum_union_of_disjoint
{α : Type u_1}
{β : Type u_2}
[inst : AddMonoid β]
[inst : DecidableEq α]
{s : Finset α}
{t : Finset α}
(h : Disjoint s t)
(f : α → β)
(comm : Set.Pairwise { x | x ∈ s ∪ t } fun a b => AddCommute (f a) (f b))
:
Finset.noncommSum (s ∪ t) f comm = Finset.noncommSum s f (_ : Set.Pairwise ↑s fun a b => AddCommute (f a) (f b)) + Finset.noncommSum t f (_ : Set.Pairwise ↑t fun a b => AddCommute (f a) (f b))
The non-commutative version of finset.sum_union
theorem
Finset.noncommProd_union_of_disjoint
{α : Type u_1}
{β : Type u_2}
[inst : Monoid β]
[inst : DecidableEq α]
{s : Finset α}
{t : Finset α}
(h : Disjoint s t)
(f : α → β)
(comm : Set.Pairwise { x | x ∈ s ∪ t } fun a b => Commute (f a) (f b))
:
Finset.noncommProd (s ∪ t) f comm = Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) * Finset.noncommProd t f (_ : Set.Pairwise ↑t fun a b => Commute (f a) (f b))
The non-commutative version of Finset.prod_union
theorem
Finset.noncommSum_add_distrib_aux
{α : Type u_1}
{β : Type u_2}
[inst : AddMonoid β]
{s : Finset α}
{f : α → β}
{g : α → β}
(comm_ff : Set.Pairwise ↑s fun x y => AddCommute (f x) (f y))
(comm_gg : Set.Pairwise ↑s fun x y => AddCommute (g x) (g y))
(comm_gf : Set.Pairwise ↑s fun x y => AddCommute (g x) (f y))
:
Set.Pairwise ↑s fun x y =>
AddCommute (((α → β) + (α → β)) (α → β) instHAdd f g x) (((α → β) + (α → β)) (α → β) instHAdd f g y)
theorem
Finset.noncommProd_mul_distrib_aux
{α : Type u_1}
{β : Type u_2}
[inst : Monoid β]
{s : Finset α}
{f : α → β}
{g : α → β}
(comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y))
(comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
(comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y))
:
theorem
Finset.noncommSum_add_distrib
{α : Type u_1}
{β : Type u_2}
[inst : AddMonoid β]
{s : Finset α}
(f : α → β)
(g : α → β)
(comm_ff : Set.Pairwise ↑s fun x y => AddCommute (f x) (f y))
(comm_gg : Set.Pairwise ↑s fun x y => AddCommute (g x) (g y))
(comm_gf : Set.Pairwise ↑s fun x y => AddCommute (g x) (f y))
:
Finset.noncommSum s (f + g)
(_ :
Set.Pairwise ↑s fun x y =>
AddCommute (((α → β) + (α → β)) (α → β) instHAdd f g x) (((α → β) + (α → β)) (α → β) instHAdd f g y)) = Finset.noncommSum s f comm_ff + Finset.noncommSum s g comm_gg
The non-commutative version of Finset.sum_add_distrib
theorem
Finset.noncommProd_mul_distrib
{α : Type u_1}
{β : Type u_2}
[inst : Monoid β]
{s : Finset α}
(f : α → β)
(g : α → β)
(comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y))
(comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
(comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y))
:
Finset.noncommProd s (f * g)
(_ :
Set.Pairwise ↑s fun x y =>
Commute (((α → β) * (α → β)) (α → β) instHMul f g x) (((α → β) * (α → β)) (α → β) instHMul f g y)) = Finset.noncommProd s f comm_ff * Finset.noncommProd s g comm_gg
The non-commutative version of Finset.prod_mul_distrib
theorem
Finset.noncommSum_single
{ι : Type u_1}
{M : ι → Type u_2}
[inst : (i : ι) → AddMonoid (M i)]
[inst : Fintype ι]
[inst : DecidableEq ι]
(x : (i : ι) → M i)
:
Finset.noncommSum Finset.univ (fun i => Pi.single i (x i))
(_ :
∀ (i : ι),
i ∈ ↑Finset.univ → ∀ (j : ι), j ∈ ↑Finset.univ → i ≠ j → AddCommute (Pi.single i (x i)) (Pi.single j (x j))) = x
theorem
Finset.noncommProd_mul_single
{ι : Type u_1}
{M : ι → Type u_2}
[inst : (i : ι) → Monoid (M i)]
[inst : Fintype ι]
[inst : DecidableEq ι]
(x : (i : ι) → M i)
:
Finset.noncommProd Finset.univ (fun i => Pi.mulSingle i (x i))
(_ :
∀ (i : ι),
i ∈ ↑Finset.univ →
∀ (j : ι), j ∈ ↑Finset.univ → i ≠ j → Commute (Pi.mulSingle i (x i)) (Pi.mulSingle j (x j))) = x
theorem
AddMonoidHom.pi_ext
{ι : Type u_1}
{γ : Type u_3}
[inst : AddMonoid γ]
{M : ι → Type u_2}
[inst : (i : ι) → AddMonoid (M i)]
[inst : Finite ι]
[inst : DecidableEq ι]
{f : ((i : ι) → M i) →+ γ}
{g : ((i : ι) → M i) →+ γ}
(h : ∀ (i : ι) (x : M i), ↑f (Pi.single i x) = ↑g (Pi.single i x))
:
f = g
theorem
MonoidHom.pi_ext
{ι : Type u_1}
{γ : Type u_3}
[inst : Monoid γ]
{M : ι → Type u_2}
[inst : (i : ι) → Monoid (M i)]
[inst : Finite ι]
[inst : DecidableEq ι]
{f : ((i : ι) → M i) →* γ}
{g : ((i : ι) → M i) →* γ}
(h : ∀ (i : ι) (x : M i), ↑f (Pi.mulSingle i x) = ↑g (Pi.mulSingle i x))
:
f = g