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 terms
• Multiset.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_3} {β : Type u_4} (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_3} {β : Type u_4} (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_3} {β : Type u_4} (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_3} {β : Type u_4} (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_3} {β : Type u_4} (f : α → β → β) (s : Multiset α) (h : LeftCommutative f) (b : β) : Multiset.noncommFoldr f s (_ : ∀ x ∈ {x : α | x ∈ s}, ∀ y ∈ {x : α | x ∈ s}, x ≠ y → ∀ (b : β), f x (f y b) = f y (f x b)) b = Multiset.foldr f h b s

def Multiset.noncommFold {α : Type u_3} (op : α → α → α) [assoc : Std.Associative 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 ∈ s}, ∀ y ∈ {x : α | x ∈ s}, x ≠ y → ∀ (b : α), op x (op y b) = op y (op x b))

@[simp]

theorem Multiset.noncommFold_coe {α : Type u_3} (op : α → α → α) [assoc : Std.Associative 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_3} (op : α → α → α) [assoc : Std.Associative 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_3} (op : α → α → α) [assoc : Std.Associative 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_3} (op : α → α → α) [assoc : Std.Associative op] (s : Multiset α) [Std.Commutative op] (a : α) : Multiset.noncommFold op s (_ : ∀ x ∈ {x : α | x ∈ s}, ∀ y ∈ {x : α | x ∈ s}, x ≠ y → op x y = op y x) a = Multiset.fold op a s

def Multiset.noncommSum {α : Type u_3} [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

theorem Multiset.noncommSum.proof_1 {α : Type u_1} [AddMonoid α] : Std.Associative fun (x x_1 : α) => x + x_1

def Multiset.noncommProd {α : Type u_3} [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_3} [AddMonoid α] (l : List α) (comm : Set.Pairwise {x : α | x ∈ ↑l} AddCommute) : Multiset.noncommSum (↑l) comm = List.sum l

@[simp]

theorem Multiset.noncommProd_coe {α : Type u_3} [Monoid α] (l : List α) (comm : Set.Pairwise {x : α | x ∈ ↑l} Commute) : Multiset.noncommProd (↑l) comm = List.prod l

@[simp]

theorem Multiset.noncommSum_empty {α : Type u_3} [AddMonoid α] (h : Set.Pairwise {x : α | x ∈ 0} AddCommute) : Multiset.noncommSum 0 h = 0

@[simp]

theorem Multiset.noncommProd_empty {α : Type u_3} [Monoid α] (h : Set.Pairwise {x : α | x ∈ 0} Commute) : Multiset.noncommProd 0 h = 1

@[simp]

theorem Multiset.noncommSum_cons {α : Type u_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_induction {α : Type u_3} [AddMonoid α] (s : Multiset α) (comm : Set.Pairwise {x : α | x ∈ s} AddCommute) (p : α → Prop) (hom : ∀ (a b : α), p a → p b → p (a + b)) (unit : p 0) (base : ∀ x ∈ s, p x) : p (Multiset.noncommSum s comm)

theorem Multiset.noncommProd_induction {α : Type u_3} [Monoid α] (s : Multiset α) (comm : Set.Pairwise {x : α | x ∈ s} Commute) (p : α → Prop) (hom : ∀ (a b : α), p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ s, p x) : p (Multiset.noncommProd s comm)

theorem Multiset.noncommSum_map_aux {F : Type u_1} {α : Type u_3} {β : Type u_4} [AddMonoid α] [AddMonoid β] [FunLike F α β] [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_3} {β : Type u_4} [Monoid α] [Monoid β] [FunLike F α β] [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_3} {β : Type u_4} [AddMonoid α] [AddMonoid β] [FunLike F α β] [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_3} {β : Type u_4} [Monoid α] [Monoid β] [FunLike F α β] [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_3} [AddMonoid α] (s : Multiset α) (comm : Set.Pairwise {x : α | x ∈ s} AddCommute) (m : α) (h : ∀ x ∈ s, x = m) : Multiset.noncommSum s comm = Multiset.card s • m

theorem Multiset.noncommProd_eq_pow_card {α : Type u_3} [Monoid α] (s : Multiset α) (comm : Set.Pairwise {x : α | x ∈ s} Commute) (m : α) (h : ∀ x ∈ s, x = m) : Multiset.noncommProd s comm = m ^ Multiset.card s

theorem Multiset.noncommSum_eq_sum {α : Type u_6} [AddCommMonoid α] (s : Multiset α) : Multiset.noncommSum s (_ : ∀ x ∈ {x : α | x ∈ s}, ∀ x_2 ∈ {x : α | x ∈ s}, x ≠ x_2 → AddCommute x x_2) = Multiset.sum s

theorem Multiset.noncommProd_eq_prod {α : Type u_6} [CommMonoid α] (s : Multiset α) : Multiset.noncommProd s (_ : ∀ x ∈ {x : α | x ∈ s}, ∀ x_2 ∈ {x : α | x ∈ s}, x ≠ x_2 → Commute x x_2) = Multiset.prod s

theorem Multiset.noncommSum_addCommute {α : Type u_3} [AddMonoid α] (s : Multiset α) (comm : Set.Pairwise {x : α | x ∈ s} AddCommute) (y : α) (h : ∀ x ∈ s, AddCommute y x) : AddCommute y (Multiset.noncommSum s comm)

theorem Multiset.noncommProd_commute {α : Type u_3} [Monoid α] (s : Multiset α) (comm : Set.Pairwise {x : α | x ∈ s} Commute) (y : α) (h : ∀ x ∈ s, Commute y x) : Commute y (Multiset.noncommProd s comm)

theorem Multiset.mul_noncommProd_erase {α : Type u_3} [Monoid α] [DecidableEq α] (s : Multiset α) {a : α} (h : a ∈ s) (comm : Set.Pairwise {x : α | x ∈ s} Commute) (comm' : optParam (∀ x ∈ {x : α | x ∈ Multiset.erase s a}, ∀ y ∈ {x : α | x ∈ Multiset.erase s a}, x ≠ y → Commute x y) (_ : ∀ x ∈ {x : α | x ∈ Multiset.erase s a}, ∀ y ∈ {x : α | x ∈ Multiset.erase s a}, x ≠ y → Commute x y)) : a * Multiset.noncommProd (Multiset.erase s a) comm' = Multiset.noncommProd s comm

theorem Multiset.noncommProd_erase_mul {α : Type u_3} [Monoid α] [DecidableEq α] (s : Multiset α) {a : α} (h : a ∈ s) (comm : Set.Pairwise {x : α | x ∈ s} Commute) (comm' : optParam (∀ x ∈ {x : α | x ∈ Multiset.erase s a}, ∀ y ∈ {x : α | x ∈ Multiset.erase s a}, x ≠ y → Commute x y) (_ : ∀ x ∈ {x : α | x ∈ Multiset.erase s a}, ∀ y ∈ {x : α | x ∈ Multiset.erase s a}, x ≠ y → Commute x y)) : Multiset.noncommProd (Multiset.erase s a) comm' * a = Multiset.noncommProd s comm

theorem Finset.noncommSum_lemma {α : Type u_3} {β : Type u_4} [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_3} {β : Type u_4} [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_3} {β : Type u_4} [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_3} {β : Type u_4} [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_induction {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (f : α → β) (comm : Set.Pairwise ↑s fun (a b : α) => AddCommute (f a) (f b)) (p : β → Prop) (hom : ∀ (a b : β), p a → p b → p (a + b)) (unit : p 0) (base : ∀ x ∈ s, p (f x)) : p (Finset.noncommSum s f comm)

theorem Finset.noncommProd_induction {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (f : α → β) (comm : Set.Pairwise ↑s fun (a b : α) => Commute (f a) (f b)) (p : β → Prop) (hom : ∀ (a b : β), p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ s, p (f x)) : p (Finset.noncommProd s f comm)

theorem Finset.noncommSum_congr {α : Type u_3} {β : Type u_4} [AddMonoid β] {s₁ : Finset α} {s₂ : Finset α} {f : α → β} {g : α → β} (h₁ : s₁ = s₂) (h₂ : ∀ 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 ∈ ↑s₂, ∀ y ∈ ↑s₂, x ≠ y → (fun (a b : α) => AddCommute (g a) (g b)) x y)

theorem Finset.noncommProd_congr {α : Type u_3} {β : Type u_4} [Monoid β] {s₁ : Finset α} {s₂ : Finset α} {f : α → β} {g : α → β} (h₁ : s₁ = s₂) (h₂ : ∀ 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 ∈ ↑s₂, ∀ y ∈ ↑s₂, x ≠ y → (fun (a b : α) => Commute (g a) (g b)) x y)

@[simp]

theorem Finset.noncommSum_toFinset {α : Type u_3} {β : Type u_4} [AddMonoid β] [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_3} {β : Type u_4} [Monoid β] [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_3} {β : Type u_4} [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_3} {β : Type u_4} [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_3} {β : Type u_4} [AddMonoid β] [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_3} {β : Type u_4} [Monoid β] [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_3} {β : Type u_4} [AddMonoid β] [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_3} {β : Type u_4} [Monoid β] [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_3} {β : Type u_4} [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_3} {β : Type u_4} [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_3} {β : Type u_4} {γ : Type u_5} [AddMonoid β] [AddMonoid γ] [FunLike F β γ] [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 ∈ ↑s, ∀ y ∈ ↑s, x ≠ y → AddCommute (g (f x)) (g (f y)))

theorem Finset.noncommProd_map {F : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Monoid β] [Monoid γ] [FunLike F β γ] [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 ∈ ↑s, ∀ y ∈ ↑s, x ≠ y → Commute (g (f x)) (g (f y)))

theorem Finset.noncommSum_eq_card_nsmul {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (f : α → β) (comm : Set.Pairwise ↑s fun (a b : α) => AddCommute (f a) (f b)) (m : β) (h : ∀ x ∈ s, f x = m) : Finset.noncommSum s f comm = s.card • m

theorem Finset.noncommProd_eq_pow_card {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (f : α → β) (comm : Set.Pairwise ↑s fun (a b : α) => Commute (f a) (f b)) (m : β) (h : ∀ x ∈ s, f x = m) : Finset.noncommProd s f comm = m ^ s.card

theorem Finset.noncommSum_addCommute {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (f : α → β) (comm : Set.Pairwise ↑s fun (a b : α) => AddCommute (f a) (f b)) (y : β) (h : ∀ x ∈ s, AddCommute y (f x)) : AddCommute y (Finset.noncommSum s f comm)

theorem Finset.noncommProd_commute {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (f : α → β) (comm : Set.Pairwise ↑s fun (a b : α) => Commute (f a) (f b)) (y : β) (h : ∀ x ∈ s, Commute y (f x)) : Commute y (Finset.noncommProd s f comm)

theorem Finset.mul_noncommProd_erase {α : Type u_3} {β : Type u_4} [Monoid β] [DecidableEq α] (s : Finset α) {a : α} (h : a ∈ s) (f : α → β) (comm : Set.Pairwise ↑s fun (a b : α) => Commute (f a) (f b)) (comm' : optParam (∀ x ∈ ↑(Finset.erase s a), ∀ y ∈ ↑(Finset.erase s a), x ≠ y → (fun (a b : α) => Commute (f a) (f b)) x y) (_ : ∀ x ∈ ↑(Finset.erase s a), ∀ y ∈ ↑(Finset.erase s a), x ≠ y → (fun (a b : α) => Commute (f a) (f b)) x y)) : f a * Finset.noncommProd (Finset.erase s a) f comm' = Finset.noncommProd s f comm

theorem Finset.noncommProd_erase_mul {α : Type u_3} {β : Type u_4} [Monoid β] [DecidableEq α] (s : Finset α) {a : α} (h : a ∈ s) (f : α → β) (comm : Set.Pairwise ↑s fun (a b : α) => Commute (f a) (f b)) (comm' : optParam (∀ x ∈ ↑(Finset.erase s a), ∀ y ∈ ↑(Finset.erase s a), x ≠ y → (fun (a b : α) => Commute (f a) (f b)) x y) (_ : ∀ x ∈ ↑(Finset.erase s a), ∀ y ∈ ↑(Finset.erase s a), x ≠ y → (fun (a b : α) => Commute (f a) (f b)) x y)) : Finset.noncommProd (Finset.erase s a) f comm' * f a = Finset.noncommProd s f comm

theorem Finset.noncommSum_eq_sum {α : Type u_3} {β : Type u_6} [AddCommMonoid β] (s : Finset α) (f : α → β) : Finset.noncommSum s f (_ : ∀ x ∈ ↑s, ∀ x_2 ∈ ↑s, x ≠ x_2 → AddCommute (f x) (f x_2)) = Finset.sum s f

theorem Finset.noncommProd_eq_prod {α : Type u_3} {β : Type u_6} [CommMonoid β] (s : Finset α) (f : α → β) : Finset.noncommProd s f (_ : ∀ x ∈ ↑s, ∀ x_2 ∈ ↑s, x ≠ x_2 → Commute (f x) (f x_2)) = Finset.prod s f

theorem Finset.noncommSum_union_of_disjoint {α : Type u_3} {β : Type u_4} [AddMonoid β] [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_3} {β : Type u_4} [Monoid β] [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_3} {β : Type u_4} [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 ((f + g) x) ((f + g) y)

theorem Finset.noncommProd_mul_distrib_aux {α : Type u_3} {β : Type u_4} [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)) : Set.Pairwise ↑s fun (x y : α) => Commute ((f * g) x) ((f * g) y)

theorem Finset.noncommSum_add_distrib {α : Type u_3} {β : Type u_4} [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 ((f + g) x) ((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_3} {β : Type u_4} [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 ((f * g) x) ((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_2} {M : ι → Type u_6} [(i : ι) → AddMonoid (M i)] [Fintype ι] [DecidableEq ι] (x : (i : ι) → M i) : Finset.noncommSum Finset.univ (fun (i : ι) => Pi.single i (x i)) (_ : ∀ i ∈ ↑Finset.univ, ∀ j ∈ ↑Finset.univ, i ≠ j → AddCommute (Pi.single i (x i)) (Pi.single j (x j))) = x

theorem Finset.noncommProd_mul_single {ι : Type u_2} {M : ι → Type u_6} [(i : ι) → Monoid (M i)] [Fintype ι] [DecidableEq ι] (x : (i : ι) → M i) : Finset.noncommProd Finset.univ (fun (i : ι) => Pi.mulSingle i (x i)) (_ : ∀ i ∈ ↑Finset.univ, ∀ j ∈ ↑Finset.univ, i ≠ j → Commute (Pi.mulSingle i (x i)) (Pi.mulSingle j (x j))) = x

theorem AddMonoidHom.pi_ext {ι : Type u_2} {γ : Type u_5} [AddMonoid γ] {M : ι → Type u_6} [(i : ι) → AddMonoid (M i)] [Finite ι] [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_2} {γ : Type u_5} [Monoid γ] {M : ι → Type u_6} [(i : ι) → Monoid (M i)] [Finite ι] [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