Mathlib.Data.Finset.NoncommProd

Multiset.noncommFoldr definition

(s : Multiset α) (comm : {x | x ∈ s}.Pairwise fun x y => ∀ b, f x (f y b) = f y (f x b)) (b : β) : β

Full source

/-- Fold of a `s : Multiset α` with `f : α → β → β`, given a proof that `LeftCommutative f`
on all elements `x ∈ s`. -/
def noncommFoldr (s : Multiset α)
    (comm : { x | x ∈ s }.Pairwise fun x y => ∀ b, f x (f y b) = f y (f x b)) (b : β) : β :=
  letI : LeftCommutative (α := { x // x ∈ s }) (f ∘ Subtype.val) :=
    ⟨fun ⟨_, hx⟩ ⟨_, hy⟩ =>
      haveI : IsRefl α fun x y => ∀ b, f x (f y b) = f y (f x b) := ⟨fun _ _ => rfl⟩
      comm.of_refl hx hy⟩
  s.attach.foldr (f ∘ Subtype.val) b

Right fold over a multiset with pairwise commutative operation

Informal description

Given a multiset $s$ over a type $\alpha$, a binary operation $f : \alpha \to \beta \to \beta$, and a proof that $f$ is pairwise commutative on the elements of $s$ (i.e., for any two distinct elements $x, y \in s$, the operations $f(x, \cdot)$ and $f(y, \cdot)$ commute), the function `noncommFoldr` computes the right fold of $f$ over $s$ starting from an initial value $b \in \beta$. This is well-defined because the result is invariant under permutations of the elements in $s$ due to the pairwise commutativity condition.

Multiset.noncommFoldr_coe theorem

(l : List α) (comm) (b : β) : noncommFoldr f (l : Multiset α) comm b = l.foldr f b

Full source

@[simp]
theorem noncommFoldr_coe (l : List α) (comm) (b : β) :
    noncommFoldr f (l : Multiset α) comm b = l.foldr f b := by
  simp only [noncommFoldr, coe_foldr, coe_attach, List.attach, List.attachWith, Function.comp_def]
  rw [← List.foldr_map]
  simp [List.map_pmap]

Equivalence of Noncommutative Right Fold and List Right Fold

Informal description

For any list $l$ of elements of type $\alpha$, any binary operation $f : \alpha \to \beta \to \beta$, and any proof `comm` that $f$ is pairwise commutative on the elements of $l$ (viewed as a multiset), the noncommutative right fold of $f$ over the multiset corresponding to $l$ with initial value $b \in \beta$ is equal to the standard right fold of $f$ over the list $l$ with initial value $b$.

Multiset.noncommFoldr_empty theorem

(h) (b : β) : noncommFoldr f (0 : Multiset α) h b = b

Full source

@[simp]
theorem noncommFoldr_empty (h) (b : β) : noncommFoldr f (0 : Multiset α) h b = b :=
  rfl

Right Fold over Empty Multiset Yields Initial Value

Informal description

For any binary operation $f : \alpha \to \beta \to \beta$ and any initial value $b \in \beta$, the right fold of $f$ over the empty multiset $0$ (with any commutativity proof $h$) equals $b$.

Multiset.noncommFoldr_cons theorem

(s : Multiset α) (a : α) (h h') (b : β) : noncommFoldr f (a ::ₘ s) h b = f a (noncommFoldr f s h' b)

Full source

theorem noncommFoldr_cons (s : Multiset α) (a : α) (h h') (b : β) :
    noncommFoldr f (a ::ₘ s) h b = f a (noncommFoldr f s h' b) := by
  induction s using Quotient.inductionOn
  simp

Right Fold Recursion for Noncommutative Operation on Multiset Cons

Informal description

For any multiset $s$ over a type $\alpha$, any element $a \in \alpha$, any binary operation $f : \alpha \to \beta \to \beta$, and any proofs $h$ and $h'$ that $f$ is pairwise commutative on the elements of $a ::ₘ s$ and $s$ respectively, the right fold of $f$ over the multiset $a ::ₘ s$ with initial value $b \in \beta$ equals $f$ applied to $a$ and the right fold of $f$ over $s$ with initial value $b$.

Multiset.noncommFoldr_eq_foldr theorem

 (s : Multiset α) [h : LeftCommutative f] (b : β) : noncommFoldr f s (fun x _ y _ _ => h.left_comm x y) b = foldr f b s

Full source

theorem noncommFoldr_eq_foldr (s : Multiset α) [h : LeftCommutative f] (b : β) :
    noncommFoldr f s (fun x _ y _ _ => h.left_comm x y) b = foldr f b s := by
  induction s using Quotient.inductionOn
  simp

Equality of Noncommutative and Standard Right Folds for Left-Commutative Operations

Informal description

For any multiset $s$ over a type $\alpha$ and a left-commutative operation $f : \alpha \to \beta \to \beta$, the noncommutative right fold of $f$ over $s$ with initial value $b \in \beta$ (using the left-commutativity property as the commutativity proof) is equal to the standard right fold of $f$ over $s$ with the same initial value $b$.

Multiset.noncommFold definition

(s : Multiset α) (comm : {x | x ∈ s}.Pairwise fun x y => op x y = op y x) : α → α

Full source

/-- Fold of a `s : Multiset α` with an associative `op : α → α → α`, given a proofs that `op`
is commutative on all elements `x ∈ s`. -/
def noncommFold (s : Multiset α) (comm : { x | x ∈ s }.Pairwise fun x y => op x y = op y x) :
    α → α :=
  noncommFoldr op s fun x hx y hy h b => by rw [← assoc.assoc, comm hx hy h, assoc.assoc]

Fold over a multiset with pairwise commutative operation

Informal description

Given a multiset $s$ over a type $\alpha$ and a binary operation $\mathrm{op} : \alpha \to \alpha \to \alpha$ that is associative, the function $\mathrm{noncommFold}$ computes the fold of $\mathrm{op}$ over $s$, provided that $\mathrm{op}$ is commutative on all pairs of distinct elements in $s$. More precisely, for any two distinct elements $x, y \in s$, we must have $\mathrm{op}\,x\,y = \mathrm{op}\,y\,x$. The fold is well-defined because the result is invariant under permutations of the elements in $s$ due to the pairwise commutativity condition.

Multiset.noncommFold_coe theorem

(l : List α) (comm) (a : α) : noncommFold op (l : Multiset α) comm a = l.foldr op a

Full source

@[simp]
theorem noncommFold_coe (l : List α) (comm) (a : α) :
    noncommFold op (l : Multiset α) comm a = l.foldr op a := by simp [noncommFold]

Equivalence of Noncommutative Fold and List Fold for Pairwise Commutative Operations

Informal description

For any list $l$ of elements of type $\alpha$, any binary operation $\mathrm{op} : \alpha \to \alpha \to \alpha$, and any proof $\mathrm{comm}$ that $\mathrm{op}$ is pairwise commutative on the elements of $l$ (viewed as a multiset), the noncommutative fold of $\mathrm{op}$ over the multiset corresponding to $l$ with initial value $a \in \alpha$ is equal to the standard right fold of $\mathrm{op}$ over the list $l$ with initial value $a$.

Multiset.noncommFold_empty theorem

(h) (a : α) : noncommFold op (0 : Multiset α) h a = a

Full source

@[simp]
theorem noncommFold_empty (h) (a : α) : noncommFold op (0 : Multiset α) h a = a :=
  rfl

Empty Multiset Fold Yields Identity Element

Informal description

For any associative binary operation $\mathrm{op} : \alpha \to \alpha \to \alpha$ and any element $a \in \alpha$, the fold of $\mathrm{op}$ over the empty multiset $0$ with any commutativity condition $h$ yields $a$, i.e., $\mathrm{noncommFold}\, \mathrm{op}\, 0\, h\, a = a$.

Multiset.noncommFold_cons theorem

(s : Multiset α) (a : α) (h h') (x : α) : noncommFold op (a ::ₘ s) h x = op a (noncommFold op s h' x)

Full source

theorem noncommFold_cons (s : Multiset α) (a : α) (h h') (x : α) :
    noncommFold op (a ::ₘ s) h x = op a (noncommFold op s h' x) := by
  induction s using Quotient.inductionOn
  simp

Recursive Formula for Noncommutative Fold over Multiset Cons

Informal description

Let $\alpha$ be a type with a binary operation $\mathrm{op} : \alpha \to \alpha \to \alpha$. For any multiset $s$ over $\alpha$, any element $a \in \alpha$, and any proofs $h$ and $h'$ that $\mathrm{op}$ is pairwise commutative on the elements of $a ::ₘ s$ and $s$ respectively, the fold of $\mathrm{op}$ over the multiset $a ::ₘ s$ with initial value $x \in \alpha$ satisfies: \[ \mathrm{noncommFold}\, \mathrm{op}\, (a ::ₘ s)\, h\, x = \mathrm{op}\, a\, (\mathrm{noncommFold}\, \mathrm{op}\, s\, h'\, x) \]

Multiset.noncommFold_eq_fold theorem

 (s : Multiset α) [Std.Commutative op] (a : α) :
  noncommFold op s (fun x _ y _ _ => Std.Commutative.comm x y) a = fold op a s

Full source

theorem noncommFold_eq_fold (s : Multiset α) [Std.Commutative op] (a : α) :
    noncommFold op s (fun x _ y _ _ => Std.Commutative.comm x y) a = fold op a s := by
  induction s using Quotient.inductionOn
  simp

Noncommutative Fold Equals Commutative Fold for Commutative Operations

Informal description

For any multiset $s$ over a type $\alpha$ with a commutative binary operation $\mathrm{op} : \alpha \to \alpha \to \alpha$ and any element $a \in \alpha$, the noncommutative fold of $\mathrm{op}$ over $s$ with initial value $a$ is equal to the standard commutative fold of $\mathrm{op}$ over $s$ with initial value $a$.

Multiset.noncommProd definition

(s : Multiset α) (comm : {x | x ∈ s}.Pairwise Commute) : α

Full source

/-- Product of a `s : Multiset α` with `[Monoid α]`, given a proof that `*` commutes
on all elements `x ∈ s`. -/
@[to_additive
      "Sum of a `s : Multiset α` with `[AddMonoid α]`, given a proof that `+` commutes
      on all elements `x ∈ s`."]
def noncommProd (s : Multiset α) (comm : { x | x ∈ s }.Pairwise Commute) : α :=
  s.noncommFold (· * ·) comm 1

Product of a multiset with pairwise commuting elements

Informal description

Given a multiset $s$ over a monoid $\alpha$ and a proof that all elements in $s$ pairwise commute, the function $\mathrm{noncommProd}$ computes the product of all elements in $s$. This is defined via $\mathrm{noncommFold}$ with multiplication as the operation and $1$ as the initial value.

Multiset.noncommProd_coe theorem

(l : List α) (comm) : noncommProd (l : Multiset α) comm = l.prod

Full source

@[to_additive (attr := simp)]
theorem noncommProd_coe (l : List α) (comm) : noncommProd (l : Multiset α) comm = l.prod := by
  rw [noncommProd]
  simp only [noncommFold_coe]
  induction' l with hd tl hl
  · simp
  · rw [List.prod_cons, List.foldr, hl]
    intro x hx y hy
    exact comm (List.mem_cons_of_mem _ hx) (List.mem_cons_of_mem _ hy)

Equality of Noncommutative Multiset Product and List Product for Pairwise Commuting Elements

Informal description

For any list $l$ of elements in a monoid $\alpha$, if all elements in $l$ pairwise commute (i.e., $x * y = y * x$ for any $x, y \in l$), then the noncommutative product of the multiset corresponding to $l$ equals the standard product of the list $l$.

Multiset.noncommProd_empty theorem

(h) : noncommProd (0 : Multiset α) h = 1

Full source

@[to_additive (attr := simp)]
theorem noncommProd_empty (h) : noncommProd (0 : Multiset α) h = 1 :=
  rfl

Noncommutative Product of Empty Multiset is One

Informal description

For any monoid $\alpha$, the noncommutative product of the empty multiset in $\alpha$ is equal to the multiplicative identity $1$, regardless of the commutativity proof $h$ provided.

Multiset.noncommProd_cons theorem

 (s : Multiset α) (a : α) (comm) : noncommProd (a ::ₘ s) comm = a * noncommProd s (comm.mono fun _ => mem_cons_of_mem)

Full source

@[to_additive (attr := simp)]
theorem noncommProd_cons (s : Multiset α) (a : α) (comm) :
    noncommProd (a ::ₘ s) comm = a * noncommProd s (comm.mono fun _ => mem_cons_of_mem) := by
  induction s using Quotient.inductionOn
  simp

Noncommutative product of a multiset with an added element: $\mathrm{noncommProd}(a ::ₘ s) = a * \mathrm{noncommProd}(s)$

Informal description

Let $\alpha$ be a monoid, $s$ be a multiset over $\alpha$, and $a$ be an element of $\alpha$. Suppose that all elements in the multiset $a ::ₘ s$ (obtained by adding $a$ to $s$) pairwise commute. Then the noncommutative product of $a ::ₘ s$ equals $a$ multiplied by the noncommutative product of $s$, where the commutativity proof for $s$ is obtained by restricting the original proof to the subset $s$.

Multiset.noncommProd_cons' theorem

 (s : Multiset α) (a : α) (comm) : noncommProd (a ::ₘ s) comm = noncommProd s (comm.mono fun _ => mem_cons_of_mem) * a

Full source

@[to_additive]
theorem noncommProd_cons' (s : Multiset α) (a : α) (comm) :
    noncommProd (a ::ₘ s) comm = noncommProd s (comm.mono fun _ => mem_cons_of_mem) * a := by
  induction' s using Quotient.inductionOn with s
  simp only [quot_mk_to_coe, cons_coe, noncommProd_coe, List.prod_cons]
  induction' s with hd tl IH
  · simp
  · rw [List.prod_cons, mul_assoc, ← IH, ← mul_assoc, ← mul_assoc]
    · congr 1
      apply comm.of_refl <;> simp
    · intro x hx y hy
      simp only [quot_mk_to_coe, List.mem_cons, mem_coe, cons_coe] at hx hy
      apply comm
      · cases hx <;> simp [*]
      · cases hy <;> simp [*]

Noncommutative product of a multiset with an added element: $\mathrm{noncommProd}(a ::ₘ s) = \mathrm{noncommProd}(s) * a$

Informal description

Let $\alpha$ be a monoid, $s$ be a multiset over $\alpha$, and $a$ be an element of $\alpha$. Suppose that all elements in the multiset $a ::ₘ s$ (obtained by adding $a$ to $s$) pairwise commute. Then the noncommutative product of $a ::ₘ s$ equals the noncommutative product of $s$ multiplied by $a$, where the commutativity proof for $s$ is obtained by restricting the original proof to the subset $s$.

Multiset.noncommProd_add theorem

 (s t : Multiset α) (comm) :
  noncommProd (s + t) comm =
    noncommProd s (comm.mono <| subset_of_le <| s.le_add_right t) *
      noncommProd t (comm.mono <| subset_of_le <| t.le_add_left s)

Full source

@[to_additive]
theorem noncommProd_add (s t : Multiset α) (comm) :
    noncommProd (s + t) comm =
      noncommProd s (comm.mono <| subset_of_le <| s.le_add_right t) *
        noncommProd t (comm.mono <| subset_of_le <| t.le_add_left s) := by
  rcases s with ⟨⟩
  rcases t with ⟨⟩
  simp

Noncommutative Product of Sum of Multisets: $\mathrm{noncommProd}(s + t) = \mathrm{noncommProd}(s) * \mathrm{noncommProd}(t)$

Informal description

Let $\alpha$ be a monoid, and let $s$ and $t$ be multisets over $\alpha$ such that all elements in $s + t$ pairwise commute. Then the noncommutative product of $s + t$ equals the product of the noncommutative product of $s$ and the noncommutative product of $t$, where the commutativity proofs for $s$ and $t$ are obtained by restricting the original proof to $s$ and $t$ respectively.

Multiset.noncommProd_induction theorem

 (s : Multiset α) (comm) (p : α → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ s, p x) :
  p (s.noncommProd comm)

Full source

@[to_additive]
lemma noncommProd_induction (s : Multiset α) (comm)
    (p : α → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ s, p x) :
    p (s.noncommProd comm) := by
  induction' s using Quotient.inductionOn with l
  simp only [quot_mk_to_coe, noncommProd_coe, mem_coe] at base ⊢
  exact l.prod_induction p hom unit base

Induction Principle for Noncommutative Multiset Product

Informal description

Let $s$ be a multiset over a monoid $\alpha$ such that all elements in $s$ pairwise commute. For any predicate $p$ on $\alpha$ that is multiplicative (i.e., $p(a)$ and $p(b)$ imply $p(a * b)$ for all $a, b \in \alpha$), if $p$ holds for the multiplicative identity $1$ and for every element in $s$, then $p$ holds for the noncommutative product of $s$.

Multiset.map_noncommProd_aux theorem

 [MulHomClass F α β] (s : Multiset α) (comm : {x | x ∈ s}.Pairwise Commute) (f : F) : {x | x ∈ s.map f}.Pairwise Commute

Full source

@[to_additive]
protected theorem map_noncommProd_aux [MulHomClass F α β] (s : Multiset α)
    (comm : { x | x ∈ s }.Pairwise Commute) (f : F) : { x | x ∈ s.map f }.Pairwise Commute := by
  simp only [Multiset.mem_map]
  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ _
  exact (comm.of_refl hx hy).map f

Preservation of Pairwise Commutation under Homomorphic Image of Multiset

Informal description

Let $F$ be a type of homomorphisms between multiplicative structures $\alpha$ and $\beta$ that preserve multiplication. Given a multiset $s$ over $\alpha$ such that any two distinct elements in $s$ commute, and a homomorphism $f \colon \alpha \to \beta$ in $F$, the image multiset $f(s)$ has the property that any two distinct elements in $f(s)$ commute.

Multiset.map_noncommProd theorem

 [MonoidHomClass F α β] (s : Multiset α) (comm) (f : F) :
  f (s.noncommProd comm) = (s.map f).noncommProd (Multiset.map_noncommProd_aux s comm f)

Full source

@[to_additive]
theorem map_noncommProd [MonoidHomClass F α β] (s : Multiset α) (comm) (f : F) :
    f (s.noncommProd comm) = (s.map f).noncommProd (Multiset.map_noncommProd_aux s comm f) := by
  induction s using Quotient.inductionOn
  simpa using map_list_prod f _

Homomorphism Property for Noncommutative Multiset Product: $f(\prod^* s) = \prod^* f(s)$

Informal description

Let $F$ be a type of monoid homomorphisms between monoids $\alpha$ and $\beta$. Given a multiset $s$ over $\alpha$ where all elements pairwise commute, and a homomorphism $f \colon \alpha \to \beta$ in $F$, the image of the noncommutative product of $s$ under $f$ equals the noncommutative product of the image multiset $f(s)$.

Multiset.noncommProd_eq_pow_card theorem

(s : Multiset α) (comm) (m : α) (h : ∀ x ∈ s, x = m) : s.noncommProd comm = m ^ Multiset.card s

Full source

@[to_additive noncommSum_eq_card_nsmul]
theorem noncommProd_eq_pow_card (s : Multiset α) (comm) (m : α) (h : ∀ x ∈ s, x = m) :
    s.noncommProd comm = m ^ Multiset.card s := by
  induction s using Quotient.inductionOn
  simp only [quot_mk_to_coe, noncommProd_coe, coe_card, mem_coe] at *
  exact List.prod_eq_pow_card _ m h

Noncommutative Product of Constant Multiset Equals Element to Cardinality Power

Informal description

Let $s$ be a multiset over a monoid $\alpha$ such that all elements in $s$ pairwise commute, and let $m \in \alpha$ be an element such that every element $x \in s$ equals $m$. Then the noncommutative product of all elements in $s$ equals $m$ raised to the power of the cardinality of $s$, i.e., \[ \mathrm{noncommProd}(s) = m^{|s|}. \]

Multiset.noncommProd_eq_prod theorem

{α : Type*} [CommMonoid α] (s : Multiset α) : (noncommProd s fun _ _ _ _ _ => Commute.all _ _) = prod s

Full source

@[to_additive]
theorem noncommProd_eq_prod {α : Type*} [CommMonoid α] (s : Multiset α) :
    (noncommProd s fun _ _ _ _ _ => Commute.all _ _) = prod s := by
  induction s using Quotient.inductionOn
  simp

Equality of Noncommutative and Standard Products in Commutative Monoids

Informal description

For any multiset $s$ over a commutative monoid $\alpha$, the noncommutative product of $s$ (with the trivial proof that all elements commute) equals the standard product of $s$.

Multiset.noncommProd_commute theorem

(s : Multiset α) (comm) (y : α) (h : ∀ x ∈ s, Commute y x) : Commute y (s.noncommProd comm)

Full source

@[to_additive]
theorem noncommProd_commute (s : Multiset α) (comm) (y : α) (h : ∀ x ∈ s, Commute y x) :
    Commute y (s.noncommProd comm) := by
  induction s using Quotient.inductionOn
  simp only [quot_mk_to_coe, noncommProd_coe]
  exact Commute.list_prod_right _ _ h

Commutation of Element with Noncommutative Multiset Product

Informal description

Let $s$ be a multiset of elements in a monoid $\alpha$, and suppose that all elements in $s$ pairwise commute (i.e., $x * y = y * x$ for any $x, y \in s$). If an element $y \in \alpha$ commutes with every element of $s$, then $y$ also commutes with the noncommutative product $\mathrm{noncommProd}(s)$ of all elements in $s$.

Finset.noncommProd_lemma theorem

 (s : Finset α) (f : α → β) (comm : (s : Set α).Pairwise (Commute on f)) :
  Set.Pairwise {x | x ∈ Multiset.map f s.val} Commute

Full source

/-- Proof used in definition of `Finset.noncommProd` -/
@[to_additive]
theorem noncommProd_lemma (s : Finset α) (f : α → β)
    (comm : (s : Set α).Pairwise (CommuteCommute on f)) :
    Set.Pairwise { x | x ∈ Multiset.map f s.val } Commute := by
  simp_rw [Multiset.mem_map]
  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ _
  exact comm.of_refl ha hb

Pairwise Commutation in Image of Finite Set under Function

Informal description

Let $s$ be a finite set of elements of type $\alpha$, and let $f : \alpha \to \beta$ be a function mapping elements of $\alpha$ to a monoid $\beta$. Suppose that for any two distinct elements $x, y \in s$, the images $f(x)$ and $f(y)$ commute in $\beta$. Then the multiset obtained by applying $f$ to each element of $s$ has the property that any two distinct elements in its image under $f$ commute pairwise.

Finset.noncommProd definition

(s : Finset α) (f : α → β) (comm : (s : Set α).Pairwise (Commute on f)) : β

Full source

/-- Product of a `s : Finset α` mapped with `f : α → β` with `[Monoid β]`,
given a proof that `*` commutes on all elements `f x` for `x ∈ s`. -/
@[to_additive
      "Sum of a `s : Finset α` mapped with `f : α → β` with `[AddMonoid β]`,
given a proof that `+` commutes on all elements `f x` for `x ∈ s`."]
def noncommProd (s : Finset α) (f : α → β)
    (comm : (s : Set α).Pairwise (CommuteCommute on f)) : β :=
  (s.1.map f).noncommProd <| noncommProd_lemma s f comm

Product over a finite set with pairwise commuting images

Informal description

Given a finite set $ s $ of elements of type $ \alpha $, a function $ f : \alpha \to \beta $ mapping elements to a monoid $ \beta $, and a proof that for any two distinct elements $ x, y \in s $, the images $ f(x) $ and $ f(y) $ commute in $ \beta $, the function `Finset.noncommProd` computes the product $ \prod_{x \in s} f(x) $ in $ \beta $. This product is well-defined due to the pairwise commutativity condition.

Finset.noncommProd_induction theorem

 (s : Finset α) (f : α → β) (comm) (p : β → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (unit : p 1)
  (base : ∀ x ∈ s, p (f x)) : p (s.noncommProd f comm)

Full source

@[to_additive]
lemma noncommProd_induction (s : Finset α) (f : α → β) (comm)
    (p : β → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ s, p (f x)) :
    p (s.noncommProd f comm) := by
  refine Multiset.noncommProd_induction _ _ _ hom unit fun b hb ↦ ?_
  obtain (⟨a, ha : a ∈ s, rfl : f a = b⟩) := by simpa using hb
  exact base a ha

Induction Principle for Noncommutative Product over Finite Set

Informal description

Let $s$ be a finite set of elements of type $\alpha$, $f : \alpha \to \beta$ a function to a monoid $\beta$, and assume that for any two distinct elements $x, y \in s$, the images $f(x)$ and $f(y)$ commute in $\beta$. Given a predicate $p$ on $\beta$ that is multiplicative (i.e., $p(a)$ and $p(b)$ imply $p(a * b)$ for all $a, b \in \beta$), if $p$ holds for the multiplicative identity $1$ and for $f(x)$ for every $x \in s$, then $p$ holds for the noncommutative product $\prod_{x \in s} f(x)$.

Finset.noncommProd_congr theorem

 {s₁ s₂ : Finset α} {f g : α → β} (h₁ : s₁ = s₂) (h₂ : ∀ x ∈ s₂, f x = g x) (comm) :
  noncommProd s₁ f comm =
    noncommProd s₂ g fun x hx y hy h => by
      dsimp only [Function.onFun]
      rw [← h₂ _ hx, ← h₂ _ hy]
      subst h₁
      exact comm hx hy h

Full source

@[to_additive (attr := congr)]
theorem noncommProd_congr {s₁ s₂ : Finset α} {f g : α → β} (h₁ : s₁ = s₂)
    (h₂ : ∀ x ∈ s₂, f x = g x) (comm) :
    noncommProd s₁ f comm =
      noncommProd s₂ g fun x hx y hy h => by
        dsimp only [Function.onFun]
        rw [← h₂ _ hx, ← h₂ _ hy]
        subst h₁
        exact comm hx hy h := by
  simp_rw [noncommProd, Multiset.map_congr (congr_arg _ h₁) h₂]

Congruence of Noncommutative Products under Set Equality and Pointwise Function Equality

Informal description

Let $s_1$ and $s_2$ be two finite sets of elements of type $\alpha$, and let $f, g : \alpha \to \beta$ be functions mapping elements to a monoid $\beta$. Suppose that: 1. $s_1 = s_2$, 2. For every $x \in s_2$, we have $f(x) = g(x)$, 3. The pairwise commutativity condition holds for $f$ on $s_1$ (i.e., for any distinct $x, y \in s_1$, $f(x)$ and $f(y)$ commute in $\beta$). Then the noncommutative product $\prod_{x \in s_1} f(x)$ is equal to the noncommutative product $\prod_{x \in s_2} g(x)$, where the commutativity condition for $g$ on $s_2$ is derived from the one for $f$ on $s_1$ via the equality $s_1 = s_2$ and the pointwise equality of $f$ and $g$ on $s_2$.

Finset.noncommProd_toFinset theorem

[DecidableEq α] (l : List α) (f : α → β) (comm) (hl : l.Nodup) : noncommProd l.toFinset f comm = (l.map f).prod

Full source

@[to_additive (attr := simp)]
theorem noncommProd_toFinset [DecidableEq α] (l : List α) (f : α → β) (comm) (hl : l.Nodup) :
    noncommProd l.toFinset f comm = (l.map f).prod := by
  rw [← List.dedup_eq_self] at hl
  simp [noncommProd, hl]

Equality of Noncommutative Product over Deduplicated List and List Product for Pairwise Commuting Images

Informal description

Let $l$ be a list of elements of type $\alpha$ with no duplicates, and let $f : \alpha \to \beta$ be a function mapping elements to a monoid $\beta$. Suppose that for any two distinct elements $x, y \in l$, the images $f(x)$ and $f(y)$ commute in $\beta$. Then the noncommutative product of $f$ over the finite set obtained from $l$ (by removing duplicates) is equal to the product of $f$ applied to each element of $l$, i.e., \[ \prod_{x \in \text{toFinset } l} f(x) = \prod_{x \in l} f(x). \]

Finset.noncommProd_empty theorem

(f : α → β) (h) : noncommProd (∅ : Finset α) f h = 1

Full source

@[to_additive (attr := simp)]
theorem noncommProd_empty (f : α → β) (h) : noncommProd (∅ : Finset α) f h = 1 :=
  rfl

Empty Noncommutative Product Yields Identity

Informal description

For any function $f \colon \alpha \to \beta$ mapping to a monoid $\beta$, and any proof $h$ of pairwise commutativity (which is vacuously true for the empty set), the noncommutative product over the empty finite set is equal to the multiplicative identity $1$ in $\beta$, i.e., \[ \prod_{x \in \emptyset} f(x) = 1. \]

Finset.noncommProd_cons theorem

 (s : Finset α) (a : α) (f : α → β) (ha : a ∉ s) (comm) :
  noncommProd (cons a s ha) f comm = f a * noncommProd s f (comm.mono fun _ => Finset.mem_cons.2 ∘ .inr)

Full source

@[to_additive (attr := simp)]
theorem noncommProd_cons (s : Finset α) (a : α) (f : α → β)
    (ha : a ∉ s) (comm) :
    noncommProd (cons a s ha) f comm =
      f a * noncommProd s f (comm.mono fun _ => Finset.mem_consFinset.mem_cons.2 ∘ .inr) := by
  simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons]

Noncommutative Product over Finite Set with Added Element: $\prod_{\text{cons}(a, s, ha)} f = f(a) * \prod_s f$

Informal description

Let $\alpha$ and $\beta$ be types, with $\beta$ equipped with a monoid structure. Given a finite set $s \subseteq \alpha$, an element $a \in \alpha$ not in $s$, a function $f : \alpha \to \beta$, and a proof that the images of any two distinct elements in $\text{cons}(a, s, ha)$ commute under $f$, the noncommutative product over $\text{cons}(a, s, ha)$ satisfies: \[ \prod_{x \in \text{cons}(a, s, ha)} f(x) = f(a) * \prod_{x \in s} f(x), \] where the commutativity condition for the product over $s$ is derived from the original condition by restricting to elements in $s$.

Finset.noncommProd_cons' theorem

 (s : Finset α) (a : α) (f : α → β) (ha : a ∉ s) (comm) :
  noncommProd (cons a s ha) f comm = noncommProd s f (comm.mono fun _ => Finset.mem_cons.2 ∘ .inr) * f a

Full source

@[to_additive]
theorem noncommProd_cons' (s : Finset α) (a : α) (f : α → β)
    (ha : a ∉ s) (comm) :
    noncommProd (cons a s ha) f comm =
      noncommProd s f (comm.mono fun _ => Finset.mem_consFinset.mem_cons.2 ∘ .inr) * f a := by
  simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons']

Noncommutative Product Formula for Extended Finite Set: $\prod_{\text{cons}(a,s)} f = (\prod_s f) * f(a)$

Informal description

Let $\alpha$ and $\beta$ be types, with $\beta$ equipped with a monoid structure. Given a finite set $s \subseteq \alpha$, an element $a \in \alpha$ not in $s$ (with proof $ha$), a function $f : \alpha \to \beta$, and a proof that the images of any two distinct elements in $\text{cons}(a, s, ha)$ commute pairwise, the noncommutative product satisfies: \[ \prod_{x \in \text{cons}(a, s, ha)} f(x) = \left(\prod_{x \in s} f(x)\right) * f(a), \] where the commutativity condition for $s$ is derived by restricting the original pairwise commutativity proof to $s$.

Finset.noncommProd_insert_of_not_mem theorem

 [DecidableEq α] (s : Finset α) (a : α) (f : α → β) (comm) (ha : a ∉ s) :
  noncommProd (insert a s) f comm = f a * noncommProd s f (comm.mono fun _ => mem_insert_of_mem)

Full source

@[to_additive (attr := simp)]
theorem noncommProd_insert_of_not_mem [DecidableEq α] (s : Finset α) (a : α) (f : α → β) (comm)
    (ha : a ∉ s) :
    noncommProd (insert a s) f comm =
      f a * noncommProd s f (comm.mono fun _ => mem_insert_of_mem) := by
  simp only [← cons_eq_insert _ _ ha, noncommProd_cons]

Noncommutative Product Formula for Insertion: $\prod_{\text{insert}(a,s)} f = f(a) * \prod_s f$

Informal description

Let $\alpha$ be a type with decidable equality and $\beta$ a monoid. Given a finite set $s \subseteq \alpha$, an element $a \in \alpha$ not in $s$, a function $f : \alpha \to \beta$, and a proof that the images of any two distinct elements in $\text{insert}(a, s)$ commute under $f$, the noncommutative product satisfies: \[ \prod_{x \in \text{insert}(a, s)} f(x) = f(a) * \prod_{x \in s} f(x), \] where the commutativity condition for the product over $s$ is derived by restricting the original pairwise commutativity proof to elements in $s$.

Finset.noncommProd_insert_of_not_mem' theorem

 [DecidableEq α] (s : Finset α) (a : α) (f : α → β) (comm) (ha : a ∉ s) :
  noncommProd (insert a s) f comm = noncommProd s f (comm.mono fun _ => mem_insert_of_mem) * f a

Full source

@[to_additive]
theorem noncommProd_insert_of_not_mem' [DecidableEq α] (s : Finset α) (a : α) (f : α → β) (comm)
    (ha : a ∉ s) :
    noncommProd (insert a s) f comm =
      noncommProd s f (comm.mono fun _ => mem_insert_of_mem) * f a := by
  simp only [← cons_eq_insert _ _ ha, noncommProd_cons']

Noncommutative Product Formula for Inserted Element: $\prod_{\text{insert}(a,s)} f = (\prod_s f) * f(a)$

Informal description

Let $\alpha$ be a type with decidable equality and $\beta$ be a monoid. Given a finite set $s \subseteq \alpha$, an element $a \in \alpha$ not in $s$ (with proof $ha$), a function $f : \alpha \to \beta$, and a proof that the images of any two distinct elements in $\text{insert}(a, s)$ commute pairwise, the noncommutative product satisfies: \[ \prod_{x \in \text{insert}(a, s)} f(x) = \left(\prod_{x \in s} f(x)\right) * f(a), \] where the commutativity condition for $s$ is derived by restricting the original pairwise commutativity proof to $s$ via the membership condition $\text{mem\_insert\_of\_mem}$.

Finset.noncommProd_singleton theorem

 (a : α) (f : α → β) :
  noncommProd ({ a } : Finset α) f
      (by
        norm_cast
        exact Set.pairwise_singleton _ _) =
    f a

Full source

@[to_additive (attr := simp)]
theorem noncommProd_singleton (a : α) (f : α → β) :
    noncommProd ({a} : Finset α) f
        (by
          norm_cast
          exact Set.pairwise_singleton _ _) =
      f a := mul_one _

Noncommutative Product over Singleton Set: $\prod_{x \in \{a\}} f(x) = f(a)$

Informal description

For any element $a$ of type $\alpha$ and any function $f \colon \alpha \to \beta$ where $\beta$ is a monoid, the noncommutative product of $f$ over the singleton finite set $\{a\}$ is equal to $f(a)$. Here, the pairwise commutativity condition is automatically satisfied since a singleton set trivially satisfies any pairwise relation.

Finset.map_noncommProd theorem

 [MonoidHomClass F β γ] (s : Finset α) (f : α → β) (comm) (g : F) :
  g (s.noncommProd f comm) = s.noncommProd (fun i => g (f i)) fun _ hx _ hy _ => (comm.of_refl hx hy).map g

Full source

@[to_additive]
theorem map_noncommProd [MonoidHomClass F β γ] (s : Finset α) (f : α → β) (comm) (g : F) :
    g (s.noncommProd f comm) =
      s.noncommProd (fun i => g (f i)) fun _ hx _ hy _ => (comm.of_refl hx hy).map g := by
  simp [noncommProd, Multiset.map_noncommProd]

Homomorphism Property for Noncommutative Finite Product: $g(\prod_{x \in s} f(x)) = \prod_{x \in s} g(f(x))$

Informal description

Let $F$ be a type of monoid homomorphisms from $\beta$ to $\gamma$, $s$ a finite set of elements of type $\alpha$, $f \colon \alpha \to \beta$ a function, and $g \colon \beta \to \gamma$ a monoid homomorphism in $F$. Suppose that for any two distinct elements $x, y \in s$, the images $f(x)$ and $f(y)$ commute in $\beta$. Then the image under $g$ of the noncommutative product $\prod_{x \in s} f(x)$ equals the noncommutative product $\prod_{x \in s} g(f(x))$, where the latter product is well-defined because the pairwise commutativity condition is preserved under $g$.

Finset.noncommProd_eq_pow_card theorem

(s : Finset α) (f : α → β) (comm) (m : β) (h : ∀ x ∈ s, f x = m) : s.noncommProd f comm = m ^ s.card

Full source

@[to_additive noncommSum_eq_card_nsmul]
theorem noncommProd_eq_pow_card (s : Finset α) (f : α → β) (comm) (m : β) (h : ∀ x ∈ s, f x = m) :
    s.noncommProd f comm = m ^ s.card := by
  rw [noncommProd, Multiset.noncommProd_eq_pow_card _ _ m]
  · simp only [Finset.card_def, Multiset.card_map]
  · simpa using h

Noncommutative Product of Constant Function Equals Element to Cardinality Power

Informal description

Let $s$ be a finite set of elements of type $\alpha$, $f \colon \alpha \to \beta$ a function to a monoid $\beta$, and assume that for any two distinct elements $x, y \in s$, the images $f(x)$ and $f(y)$ commute in $\beta$. If there exists an element $m \in \beta$ such that $f(x) = m$ for all $x \in s$, then the noncommutative product $\prod_{x \in s} f(x)$ equals $m$ raised to the power of the cardinality of $s$, i.e., \[ \prod_{x \in s} f(x) = m^{|s|}. \]

Finset.noncommProd_commute theorem

(s : Finset α) (f : α → β) (comm) (y : β) (h : ∀ x ∈ s, Commute y (f x)) : Commute y (s.noncommProd f comm)

Full source

@[to_additive]
theorem noncommProd_commute (s : Finset α) (f : α → β) (comm) (y : β)
    (h : ∀ x ∈ s, Commute y (f x)) : Commute y (s.noncommProd f comm) := by
  apply Multiset.noncommProd_commute
  intro y
  rw [Multiset.mem_map]
  rintro ⟨x, ⟨hx, rfl⟩⟩
  exact h x hx

Commutation of Element with Noncommutative Finite Product

Informal description

Let $s$ be a finite set of elements of type $\alpha$, $f \colon \alpha \to \beta$ a function into a monoid $\beta$, and suppose that for any two distinct elements $x, y \in s$, the images $f(x)$ and $f(y)$ commute in $\beta$. If an element $y \in \beta$ commutes with $f(x)$ for every $x \in s$, then $y$ commutes with the noncommutative product $\prod_{x \in s} f(x)$.

Finset.noncommProd_eq_prod theorem

 {β : Type*} [CommMonoid β] (s : Finset α) (f : α → β) : (noncommProd s f fun _ _ _ _ _ => Commute.all _ _) = s.prod f

Full source

@[to_additive]
theorem noncommProd_eq_prod {β : Type*} [CommMonoid β] (s : Finset α) (f : α → β) :
    (noncommProd s f fun _ _ _ _ _ => Commute.all _ _) = s.prod f := by
  induction' s using Finset.cons_induction_on with a s ha IH
  · simp
  · simp [ha, IH]

Noncommutative Product Equals Standard Product in Commutative Monoid

Informal description

For any finite set $s$ of elements of type $\alpha$ and any function $f \colon \alpha \to \beta$ into a commutative monoid $\beta$, the noncommutative product $\prod_{x \in s} f(x)$ (with the trivial commutativity condition) equals the standard product $\prod_{x \in s} f(x)$.

Finset.noncommProd_union_of_disjoint theorem

 [DecidableEq α] {s t : Finset α} (h : Disjoint s t) (f : α → β) (comm : {x | x ∈ s ∪ t}.Pairwise (Commute on f)) :
  noncommProd (s ∪ t) f comm =
    noncommProd s f (comm.mono <| coe_subset.2 subset_union_left) *
      noncommProd t f (comm.mono <| coe_subset.2 subset_union_right)

Full source

/-- The non-commutative version of `Finset.prod_union` -/
@[to_additive "The non-commutative version of `Finset.sum_union`"]
theorem noncommProd_union_of_disjoint [DecidableEq α] {s t : Finset α} (h : Disjoint s t)
    (f : α → β) (comm : { x | x ∈ s ∪ t }.Pairwise (CommuteCommute on f)) :
    noncommProd (s ∪ t) f comm =
      noncommProd s f (comm.mono <| coe_subset.2 subset_union_left) *
        noncommProd t f (comm.mono <| coe_subset.2 subset_union_right) := by
  obtain ⟨sl, sl', rfl⟩ := exists_list_nodup_eq s
  obtain ⟨tl, tl', rfl⟩ := exists_list_nodup_eq t
  rw [List.disjoint_toFinset_iff_disjoint] at h
  calc noncommProd (List.toFinsetList.toFinset sl ∪ List.toFinset tl) f comm
     = noncommProd ⟨↑(sl ++ tl), Multiset.coe_nodup.2 (sl'.append tl' h)⟩ f
         (by convert comm; simp [Set.ext_iff]) := noncommProd_congr (by ext; simp) (by simp) _
   _ = noncommProd (List.toFinset sl) f (comm.mono <| coe_subset.2 subset_union_left) *
         noncommProd (List.toFinset tl) f (comm.mono <| coe_subset.2 subset_union_right) := by
    simp [noncommProd, List.dedup_eq_self.2 sl', List.dedup_eq_self.2 tl', h]

Noncommutative Product over Union of Disjoint Finite Sets

Informal description

Let $s$ and $t$ be disjoint finite sets of elements of type $\alpha$ (with decidable equality), and let $f : \alpha \to \beta$ be a function into a monoid $\beta$. Suppose that for any two distinct elements $x, y \in s \cup t$, the images $f(x)$ and $f(y)$ commute in $\beta$. Then the noncommutative product over $s \cup t$ satisfies: \[ \prod_{x \in s \cup t} f(x) = \left(\prod_{x \in s} f(x)\right) * \left(\prod_{x \in t} f(x)\right), \] where the commutativity conditions for the products over $s$ and $t$ are inherited from the condition on $s \cup t$.

Finset.noncommProd_mul_distrib_aux theorem

 {s : Finset α} {f : α → β} {g : α → β} (comm_ff : (s : Set α).Pairwise (Commute on f))
  (comm_gg : (s : Set α).Pairwise (Commute on g)) (comm_gf : (s : Set α).Pairwise fun x y => Commute (g x) (f y)) :
  (s : Set α).Pairwise fun x y => Commute ((f * g) x) ((f * g) y)

Full source

@[to_additive]
theorem noncommProd_mul_distrib_aux {s : Finset α} {f : α → β} {g : α → β}
    (comm_ff : (s : Set α).Pairwise (CommuteCommute on f))
    (comm_gg : (s : Set α).Pairwise (CommuteCommute on g))
    (comm_gf : (s : Set α).Pairwise fun x y => Commute (g x) (f y)) :
    (s : Set α).Pairwise fun x y => Commute ((f * g) x) ((f * g) y) := by
  intro x hx y hy h
  apply Commute.mul_left <;> apply Commute.mul_right
  · exact comm_ff.of_refl hx hy
  · exact (comm_gf hy hx h.symm).symm
  · exact comm_gf hx hy h
  · exact comm_gg.of_refl hx hy

Pairwise Commutation of Pointwise Product under Commutation Hypotheses

Informal description

Let $s$ be a finite set of type $\alpha$, and let $f, g : \alpha \to \beta$ be functions into a monoid $\beta$. Suppose that: 1. The elements of $f$ pairwise commute on $s$ (i.e., for any distinct $x, y \in s$, $f(x)$ and $f(y)$ commute), 2. The elements of $g$ pairwise commute on $s$ (i.e., for any distinct $x, y \in s$, $g(x)$ and $g(y)$ commute), 3. For any distinct $x, y \in s$, $g(x)$ commutes with $f(y)$. Then, the elements of the pointwise product $f * g$ (defined by $(f * g)(x) = f(x) * g(x)$) also pairwise commute on $s$.

Finset.noncommProd_mul_distrib theorem

 {s : Finset α} (f : α → β) (g : α → β) (comm_ff comm_gg comm_gf) :
  noncommProd s (f * g) (noncommProd_mul_distrib_aux comm_ff comm_gg comm_gf) =
    noncommProd s f comm_ff * noncommProd s g comm_gg

Full source

/-- The non-commutative version of `Finset.prod_mul_distrib` -/
@[to_additive "The non-commutative version of `Finset.sum_add_distrib`"]
theorem noncommProd_mul_distrib {s : Finset α} (f : α → β) (g : α → β) (comm_ff comm_gg comm_gf) :
    noncommProd s (f * g) (noncommProd_mul_distrib_aux comm_ff comm_gg comm_gf) =
      noncommProd s f comm_ff * noncommProd s g comm_gg := by
  induction' s using Finset.cons_induction_on with x s hnmem ih
  · simp
  rw [Finset.noncommProd_cons, Finset.noncommProd_cons, Finset.noncommProd_cons, Pi.mul_apply,
    ih (comm_ff.mono fun _ => mem_cons_of_mem) (comm_gg.mono fun _ => mem_cons_of_mem)
      (comm_gf.mono fun _ => mem_cons_of_mem),
    (noncommProd_commute _ _ _ _ fun y hy => ?_).mul_mul_mul_comm]
  exact comm_gf (mem_cons_self x s) (mem_cons_of_mem hy) (ne_of_mem_of_not_mem hy hnmem).symm

Distributivity of Noncommutative Product over Pointwise Multiplication

Informal description

Let $s$ be a finite set of elements of type $\alpha$, and let $f, g : \alpha \to \beta$ be functions into a monoid $\beta$. Suppose that: 1. For any distinct $x, y \in s$, $f(x)$ and $f(y)$ commute, 2. For any distinct $x, y \in s$, $g(x)$ and $g(y)$ commute, 3. For any distinct $x, y \in s$, $g(x)$ commutes with $f(y)$. Then the noncommutative product of the pointwise product $f * g$ (defined by $(f * g)(x) = f(x) * g(x)$) over $s$ satisfies: \[ \prod_{x \in s} (f(x) * g(x)) = \left(\prod_{x \in s} f(x)\right) * \left(\prod_{x \in s} g(x)\right). \]

Finset.noncommProd_mul_single theorem

 [Fintype ι] [DecidableEq ι] (x : ∀ i, M i) :
  (univ.noncommProd (fun i => Pi.mulSingle i (x i)) fun i _ j _ _ => Pi.mulSingle_apply_commute x i j) = x

Full source

@[to_additive]
theorem noncommProd_mul_single [Fintype ι] [DecidableEq ι] (x : ∀ i, M i) :
    (univ.noncommProd (fun i => Pi.mulSingle i (x i)) fun i _ j _ _ =>
        Pi.mulSingle_apply_commute x i j) = x := by
  ext i
  apply (univ.map_noncommProd (fun i ↦ MonoidHom.mulSingle M i (x i)) ?a
    (Pi.evalMonoidHom M i)).trans
  case a =>
    intro i _ j _ _
    exact Pi.mulSingle_apply_commute x i j
  convert (noncommProd_congr (insert_erase (mem_univ i)).symm _ _).trans _
  · intro j
    exact Pi.mulSingle j (x j) i
  · intro j _; dsimp
  · rw [noncommProd_insert_of_not_mem _ _ _ _ (not_mem_erase _ _),
      noncommProd_eq_pow_card (univ.erase i), one_pow, mul_one]
    · simp only [MonoidHom.mulSingle_apply, ne_eq, Pi.mulSingle_eq_same]
    · intro j hj
      simp? at hj says simp only [mem_erase, ne_eq, mem_univ, and_true] at hj
      simp only [MonoidHom.mulSingle_apply, Pi.mulSingle, Function.update, Eq.ndrec, Pi.one_apply,
        ne_eq, dite_eq_right_iff]
      intro h
      simp [*] at *

Noncommutative Product of Multiplicative Single Functions Equals Original Function

Informal description

Let $\iota$ be a finite type with decidable equality, and let $(M_i)_{i \in \iota}$ be a family of monoids. For any function $x \colon \prod_{i \in \iota} M_i$, the noncommutative product over the universal finite set $\text{univ} \subseteq \iota$ of the multiplicative single functions $\text{mulSingle}_i(x_i)$ equals $x$ itself. That is, \[ \prod_{i \in \iota} \text{mulSingle}_i(x_i) = x, \] where the product is well-defined because the multiplicative single functions pairwise commute (i.e., $\text{mulSingle}_i(x_i)$ and $\text{mulSingle}_j(x_j)$ commute for any $i, j \in \iota$).

MonoidHom.pi_ext theorem

 [Finite ι] [DecidableEq ι] {f g : (∀ i, M i) →* γ} (h : ∀ i x, f (Pi.mulSingle i x) = g (Pi.mulSingle i x)) : f = g

Full source

@[to_additive]
theorem _root_.MonoidHom.pi_ext [Finite ι] [DecidableEq ι] {f g : (∀ i, M i) →* γ}
    (h : ∀ i x, f (Pi.mulSingle i x) = g (Pi.mulSingle i x)) : f = g := by
  cases nonempty_fintype ι
  ext x
  rw [← noncommProd_mul_single x, univ.map_noncommProd, univ.map_noncommProd]
  congr 1 with i; exact h i (x i)

Extensionality of Monoid Homomorphisms via Multiplicative Single Functions

Informal description

Let $\iota$ be a finite type with decidable equality, and let $(M_i)_{i \in \iota}$ be a family of monoids. Suppose $f, g \colon \prod_{i \in \iota} M_i \to \gamma$ are monoid homomorphisms to a monoid $\gamma$. If for every index $i \in \iota$ and every element $x \in M_i$, the homomorphisms $f$ and $g$ agree on the multiplicative single function $\text{mulSingle}_i(x)$, then $f = g$.

Mathlib.Data.Finset.NoncommProd

Main definitions

Implementation details