Documentation

Mathlib.Data.Finset.NoncommProd

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 #

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 : β) :
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 : β) :
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
@[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 : α) :
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 yop 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
def Multiset.noncommSum.proof_1 {α : Type u_1} [inst : AddMonoid α] :
IsAssociative α fun x x_1 => x + x_1
Equations
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
@[simp]
theorem Multiset.noncommSum_coe {α : Type u_1} [inst : AddMonoid α] (l : List α) (comm : Set.Pairwise { x | x l } AddCommute) :
@[simp]
theorem Multiset.noncommProd_coe {α : Type u_1} [inst : Monoid α] (l : List α) (comm : Set.Pairwise { x | x l } Commute) :
@[simp]
theorem Multiset.noncommSum_empty {α : Type u_1} [inst : AddMonoid α] (h : Set.Pairwise { x | x 0 } AddCommute) :
@[simp]
theorem Multiset.noncommProd_empty {α : Type u_1} [inst : Monoid α] (h : Set.Pairwise { x | x 0 } Commute) :
@[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 sx = 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 sx = 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_2AddCommute 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_2Commute 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 sAddCommute y x) :
theorem Multiset.noncommProd_commute {α : Type u_1} [inst : Monoid α] (s : Multiset α) (comm : Set.Pairwise { x | x s } Commute) (y : α) (h : ∀ (x : α), x sCommute y x) :
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
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
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) :
@[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) :
@[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)) :
@[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)) :
@[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 sx yAddCommute (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 sx yCommute (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 sf x = 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 sf x = m) :
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 sAddCommute y (f x)) :
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 sCommute y (f x)) :
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 sx x_2AddCommute (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 sx x_2Commute (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)) :
Set.Pairwise s fun x y => Commute (((αβ) * (αβ)) (αβ) instHMul f g x) (((αβ) * (αβ)) (αβ) instHMul f g 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.univi jAddCommute (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.univi jCommute (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