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_3} {β : Type u_4} (f : αββ) (s : Multiset α) (comm : {x : α | x s}.Pairwise 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
Instances For
    @[simp]
    theorem Multiset.noncommFoldr_coe {α : Type u_3} {β : Type u_4} (f : αββ) (l : List α) (comm : {x : α | x l}.Pairwise fun (x y : α) => ∀ (b : β), f x (f y b) = f y (f x b)) (b : β) :
    Multiset.noncommFoldr f (l) comm b = List.foldr f b l
    @[simp]
    theorem Multiset.noncommFoldr_empty {α : Type u_3} {β : Type u_4} (f : αββ) (h : {x : α | x 0}.Pairwise fun (x y : α) => ∀ (b : β), f x (f y b) = f y (f x b)) (b : β) :
    theorem Multiset.noncommFoldr_cons {α : Type u_3} {β : Type u_4} (f : αββ) (s : Multiset α) (a : α) (h : {x : α | x a ::ₘ s}.Pairwise fun (x y : α) => ∀ (b : β), f x (f y b) = f y (f x b)) (h' : {x : α | x s}.Pairwise fun (x y : α) => ∀ (b : β), f x (f y b) = f y (f x b)) (b : β) :
    theorem Multiset.noncommFoldr_eq_foldr {α : Type u_3} {β : Type u_4} (f : αββ) (s : Multiset α) (h : LeftCommutative f) (b : β) :
    def Multiset.noncommFold {α : Type u_3} (op : ααα) [assoc : Std.Associative op] (s : Multiset α) (comm : {x : α | x s}.Pairwise 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
    Instances For
      @[simp]
      theorem Multiset.noncommFold_coe {α : Type u_3} (op : ααα) [assoc : Std.Associative op] (l : List α) (comm : {x : α | x l}.Pairwise fun (x y : α) => op x y = op y x) (a : α) :
      Multiset.noncommFold op (l) comm a = List.foldr op a l
      @[simp]
      theorem Multiset.noncommFold_empty {α : Type u_3} (op : ααα) [assoc : Std.Associative op] (h : {x : α | x 0}.Pairwise fun (x y : α) => op x y = op y x) (a : α) :
      theorem Multiset.noncommFold_cons {α : Type u_3} (op : ααα) [assoc : Std.Associative op] (s : Multiset α) (a : α) (h : {x : α | x a ::ₘ s}.Pairwise fun (x y : α) => op x y = op y x) (h' : {x : α | x s}.Pairwise 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 : α) :
      theorem Multiset.noncommSum.proof_1 {α : Type u_1} [AddMonoid α] :
      Std.Associative fun (x x_1 : α) => x + x_1
      def Multiset.noncommSum {α : Type u_3} [AddMonoid α] (s : Multiset α) (comm : {x : α | x s}.Pairwise AddCommute) :
      α

      Sum of a s : Multiset α with [AddMonoid α], given a proof that + commutes on all elements x ∈ s.

      Equations
      Instances For
        def Multiset.noncommProd {α : Type u_3} [Monoid α] (s : Multiset α) (comm : {x : α | x s}.Pairwise Commute) :
        α

        Product of a s : Multiset α with [Monoid α], given a proof that * commutes on all elements x ∈ s.

        Equations
        Instances For
          @[simp]
          theorem Multiset.noncommSum_coe {α : Type u_3} [AddMonoid α] (l : List α) (comm : {x : α | x l}.Pairwise AddCommute) :
          (l).noncommSum comm = l.sum
          @[simp]
          theorem Multiset.noncommProd_coe {α : Type u_3} [Monoid α] (l : List α) (comm : {x : α | x l}.Pairwise Commute) :
          (l).noncommProd comm = l.prod
          @[simp]
          theorem Multiset.noncommSum_empty {α : Type u_3} [AddMonoid α] (h : {x : α | x 0}.Pairwise AddCommute) :
          @[simp]
          theorem Multiset.noncommProd_empty {α : Type u_3} [Monoid α] (h : {x : α | x 0}.Pairwise Commute) :
          @[simp]
          theorem Multiset.noncommSum_cons {α : Type u_3} [AddMonoid α] (s : Multiset α) (a : α) (comm : {x : α | x a ::ₘ s}.Pairwise AddCommute) :
          (a ::ₘ s).noncommSum comm = a + s.noncommSum
          @[simp]
          theorem Multiset.noncommProd_cons {α : Type u_3} [Monoid α] (s : Multiset α) (a : α) (comm : {x : α | x a ::ₘ s}.Pairwise Commute) :
          (a ::ₘ s).noncommProd comm = a * s.noncommProd
          theorem Multiset.noncommSum_cons' {α : Type u_3} [AddMonoid α] (s : Multiset α) (a : α) (comm : {x : α | x a ::ₘ s}.Pairwise AddCommute) :
          (a ::ₘ s).noncommSum comm = s.noncommSum + a
          theorem Multiset.noncommProd_cons' {α : Type u_3} [Monoid α] (s : Multiset α) (a : α) (comm : {x : α | x a ::ₘ s}.Pairwise Commute) :
          (a ::ₘ s).noncommProd comm = s.noncommProd * a
          theorem Multiset.noncommSum_add {α : Type u_3} [AddMonoid α] (s : Multiset α) (t : Multiset α) (comm : {x : α | x s + t}.Pairwise AddCommute) :
          (s + t).noncommSum comm = s.noncommSum + t.noncommSum
          theorem Multiset.noncommProd_add {α : Type u_3} [Monoid α] (s : Multiset α) (t : Multiset α) (comm : {x : α | x s + t}.Pairwise Commute) :
          (s + t).noncommProd comm = s.noncommProd * t.noncommProd
          theorem Multiset.noncommSum_induction {α : Type u_3} [AddMonoid α] (s : Multiset α) (comm : {x : α | x s}.Pairwise AddCommute) (p : αProp) (hom : ∀ (a b : α), p ap bp (a + b)) (unit : p 0) (base : xs, p x) :
          p (s.noncommSum comm)
          theorem Multiset.noncommProd_induction {α : Type u_3} [Monoid α] (s : Multiset α) (comm : {x : α | x s}.Pairwise Commute) (p : αProp) (hom : ∀ (a b : α), p ap bp (a * b)) (unit : p 1) (base : xs, p x) :
          p (s.noncommProd comm)
          theorem Multiset.map_noncommSum_aux {F : Type u_1} {α : Type u_3} {β : Type u_4} [AddMonoid α] [AddMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (s : Multiset α) (comm : {x : α | x s}.Pairwise AddCommute) (f : F) :
          {x : β | x Multiset.map (f) s}.Pairwise AddCommute
          theorem Multiset.map_noncommProd_aux {F : Type u_1} {α : Type u_3} {β : Type u_4} [Monoid α] [Monoid β] [FunLike F α β] [MonoidHomClass F α β] (s : Multiset α) (comm : {x : α | x s}.Pairwise Commute) (f : F) :
          {x : β | x Multiset.map (f) s}.Pairwise Commute
          theorem Multiset.map_noncommSum {F : Type u_1} {α : Type u_3} {β : Type u_4} [AddMonoid α] [AddMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (s : Multiset α) (comm : {x : α | x s}.Pairwise AddCommute) (f : F) :
          f (s.noncommSum comm) = (Multiset.map (f) s).noncommSum
          theorem Multiset.map_noncommProd {F : Type u_1} {α : Type u_3} {β : Type u_4} [Monoid α] [Monoid β] [FunLike F α β] [MonoidHomClass F α β] (s : Multiset α) (comm : {x : α | x s}.Pairwise Commute) (f : F) :
          f (s.noncommProd comm) = (Multiset.map (f) s).noncommProd
          @[deprecated Multiset.map_noncommProd]
          theorem Multiset.noncommProd_map {F : Type u_1} {α : Type u_3} {β : Type u_4} [Monoid α] [Monoid β] [FunLike F α β] [MonoidHomClass F α β] (s : Multiset α) (comm : {x : α | x s}.Pairwise Commute) (f : F) :
          f (s.noncommProd comm) = (Multiset.map (f) s).noncommProd

          Alias of Multiset.map_noncommProd.

          @[deprecated Multiset.map_noncommSum]
          theorem Multiset.noncommSum_map {F : Type u_1} {α : Type u_3} {β : Type u_4} [AddMonoid α] [AddMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (s : Multiset α) (comm : {x : α | x s}.Pairwise AddCommute) (f : F) :
          f (s.noncommSum comm) = (Multiset.map (f) s).noncommSum

          Alias of Multiset.map_noncommSum.

          @[deprecated Multiset.map_noncommProd_aux]
          theorem Multiset.noncommProd_map_aux {F : Type u_1} {α : Type u_3} {β : Type u_4} [Monoid α] [Monoid β] [FunLike F α β] [MonoidHomClass F α β] (s : Multiset α) (comm : {x : α | x s}.Pairwise Commute) (f : F) :
          {x : β | x Multiset.map (f) s}.Pairwise Commute

          Alias of Multiset.map_noncommProd_aux.

          @[deprecated Multiset.map_noncommSum_aux]
          theorem Multiset.noncommSum_map_aux {F : Type u_1} {α : Type u_3} {β : Type u_4} [AddMonoid α] [AddMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (s : Multiset α) (comm : {x : α | x s}.Pairwise AddCommute) (f : F) :
          {x : β | x Multiset.map (f) s}.Pairwise AddCommute

          Alias of Multiset.map_noncommSum_aux.

          theorem Multiset.noncommSum_eq_card_nsmul {α : Type u_3} [AddMonoid α] (s : Multiset α) (comm : {x : α | x s}.Pairwise AddCommute) (m : α) (h : xs, x = m) :
          s.noncommSum comm = Multiset.card s m
          theorem Multiset.noncommProd_eq_pow_card {α : Type u_3} [Monoid α] (s : Multiset α) (comm : {x : α | x s}.Pairwise Commute) (m : α) (h : xs, x = m) :
          s.noncommProd comm = m ^ Multiset.card s
          theorem Multiset.noncommSum_eq_sum {α : Type u_6} [AddCommMonoid α] (s : Multiset α) :
          s.noncommSum = s.sum
          theorem Multiset.noncommProd_eq_prod {α : Type u_6} [CommMonoid α] (s : Multiset α) :
          s.noncommProd = s.prod
          theorem Multiset.noncommSum_addCommute {α : Type u_3} [AddMonoid α] (s : Multiset α) (comm : {x : α | x s}.Pairwise AddCommute) (y : α) (h : xs, AddCommute y x) :
          AddCommute y (s.noncommSum comm)
          theorem Multiset.noncommProd_commute {α : Type u_3} [Monoid α] (s : Multiset α) (comm : {x : α | x s}.Pairwise Commute) (y : α) (h : xs, Commute y x) :
          Commute y (s.noncommProd comm)
          theorem Multiset.mul_noncommProd_erase {α : Type u_3} [Monoid α] [DecidableEq α] (s : Multiset α) {a : α} (h : a s) (comm : {x : α | x s}.Pairwise Commute) (comm' : optParam (x{x : α | x s.erase a}, y{x : α | x s.erase a}, x yCommute x y) ) :
          a * (s.erase a).noncommProd comm' = s.noncommProd comm
          theorem Multiset.noncommProd_erase_mul {α : Type u_3} [Monoid α] [DecidableEq α] (s : Multiset α) {a : α} (h : a s) (comm : {x : α | x s}.Pairwise Commute) (comm' : optParam (x{x : α | x s.erase a}, y{x : α | x s.erase a}, x yCommute x y) ) :
          (s.erase a).noncommProd comm' * a = s.noncommProd comm
          theorem Finset.noncommSum_lemma {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (f : αβ) (comm : (s).Pairwise fun (a b : α) => AddCommute (f a) (f b)) :
          {x : β | x Multiset.map f s.val}.Pairwise AddCommute
          theorem Finset.noncommProd_lemma {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (f : αβ) (comm : (s).Pairwise fun (a b : α) => Commute (f a) (f b)) :
          {x : β | x Multiset.map f s.val}.Pairwise Commute

          Proof used in definition of Finset.noncommProd

          def Finset.noncommSum {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (f : αβ) (comm : (s).Pairwise 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
          Instances For
            def Finset.noncommProd {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (f : αβ) (comm : (s).Pairwise 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
            Instances For
              theorem Finset.noncommSum_induction {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (f : αβ) (comm : (s).Pairwise fun (a b : α) => AddCommute (f a) (f b)) (p : βProp) (hom : ∀ (a b : β), p ap bp (a + b)) (unit : p 0) (base : xs, p (f x)) :
              p (s.noncommSum f comm)
              theorem Finset.noncommProd_induction {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (f : αβ) (comm : (s).Pairwise fun (a b : α) => Commute (f a) (f b)) (p : βProp) (hom : ∀ (a b : β), p ap bp (a * b)) (unit : p 1) (base : xs, p (f x)) :
              p (s.noncommProd f comm)
              theorem Finset.noncommSum_congr {α : Type u_3} {β : Type u_4} [AddMonoid β] {s₁ : Finset α} {s₂ : Finset α} {f : αβ} {g : αβ} (h₁ : s₁ = s₂) (h₂ : xs₂, f x = g x) (comm : (s₁).Pairwise fun (a b : α) => AddCommute (f a) (f b)) :
              s₁.noncommSum f comm = s₂.noncommSum g
              theorem Finset.noncommProd_congr {α : Type u_3} {β : Type u_4} [Monoid β] {s₁ : Finset α} {s₂ : Finset α} {f : αβ} {g : αβ} (h₁ : s₁ = s₂) (h₂ : xs₂, f x = g x) (comm : (s₁).Pairwise fun (a b : α) => Commute (f a) (f b)) :
              s₁.noncommProd f comm = s₂.noncommProd g
              @[simp]
              theorem Finset.noncommSum_toFinset {α : Type u_3} {β : Type u_4} [AddMonoid β] [DecidableEq α] (l : List α) (f : αβ) (comm : (l.toFinset).Pairwise fun (a b : α) => AddCommute (f a) (f b)) (hl : l.Nodup) :
              l.toFinset.noncommSum f comm = (List.map f l).sum
              @[simp]
              theorem Finset.noncommProd_toFinset {α : Type u_3} {β : Type u_4} [Monoid β] [DecidableEq α] (l : List α) (f : αβ) (comm : (l.toFinset).Pairwise fun (a b : α) => Commute (f a) (f b)) (hl : l.Nodup) :
              l.toFinset.noncommProd f comm = (List.map f l).prod
              @[simp]
              theorem Finset.noncommSum_empty {α : Type u_3} {β : Type u_4} [AddMonoid β] (f : αβ) (h : ().Pairwise fun (a b : α) => AddCommute (f a) (f b)) :
              .noncommSum f h = 0
              @[simp]
              theorem Finset.noncommProd_empty {α : Type u_3} {β : Type u_4} [Monoid β] (f : αβ) (h : ().Pairwise fun (a b : α) => Commute (f a) (f b)) :
              .noncommProd f h = 1
              @[simp]
              theorem Finset.noncommSum_cons {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (a : α) (f : αβ) (ha : as) (comm : ((Finset.cons a s ha)).Pairwise fun (a b : α) => AddCommute (f a) (f b)) :
              (Finset.cons a s ha).noncommSum f comm = f a + s.noncommSum f
              @[simp]
              theorem Finset.noncommProd_cons {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (a : α) (f : αβ) (ha : as) (comm : ((Finset.cons a s ha)).Pairwise fun (a b : α) => Commute (f a) (f b)) :
              (Finset.cons a s ha).noncommProd f comm = f a * s.noncommProd f
              theorem Finset.noncommSum_cons' {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (a : α) (f : αβ) (ha : as) (comm : ((Finset.cons a s ha)).Pairwise fun (a b : α) => AddCommute (f a) (f b)) :
              (Finset.cons a s ha).noncommSum f comm = s.noncommSum f + f a
              theorem Finset.noncommProd_cons' {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (a : α) (f : αβ) (ha : as) (comm : ((Finset.cons a s ha)).Pairwise fun (a b : α) => Commute (f a) (f b)) :
              (Finset.cons a s ha).noncommProd f comm = s.noncommProd f * f a
              @[simp]
              theorem Finset.noncommSum_insert_of_not_mem {α : Type u_3} {β : Type u_4} [AddMonoid β] [DecidableEq α] (s : Finset α) (a : α) (f : αβ) (comm : ((insert a s)).Pairwise fun (a b : α) => AddCommute (f a) (f b)) (ha : as) :
              (insert a s).noncommSum f comm = f a + s.noncommSum f
              @[simp]
              theorem Finset.noncommProd_insert_of_not_mem {α : Type u_3} {β : Type u_4} [Monoid β] [DecidableEq α] (s : Finset α) (a : α) (f : αβ) (comm : ((insert a s)).Pairwise fun (a b : α) => Commute (f a) (f b)) (ha : as) :
              (insert a s).noncommProd f comm = f a * s.noncommProd f
              theorem Finset.noncommSum_insert_of_not_mem' {α : Type u_3} {β : Type u_4} [AddMonoid β] [DecidableEq α] (s : Finset α) (a : α) (f : αβ) (comm : ((insert a s)).Pairwise fun (a b : α) => AddCommute (f a) (f b)) (ha : as) :
              (insert a s).noncommSum f comm = s.noncommSum f + f a
              theorem Finset.noncommProd_insert_of_not_mem' {α : Type u_3} {β : Type u_4} [Monoid β] [DecidableEq α] (s : Finset α) (a : α) (f : αβ) (comm : ((insert a s)).Pairwise fun (a b : α) => Commute (f a) (f b)) (ha : as) :
              (insert a s).noncommProd f comm = s.noncommProd f * f a
              @[simp]
              theorem Finset.noncommSum_singleton {α : Type u_3} {β : Type u_4} [AddMonoid β] (a : α) (f : αβ) :
              {a}.noncommSum f = f a
              @[simp]
              theorem Finset.noncommProd_singleton {α : Type u_3} {β : Type u_4} [Monoid β] (a : α) (f : αβ) :
              {a}.noncommProd f = f a
              theorem Finset.map_noncommSum {F : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddMonoid β] [AddMonoid γ] [FunLike F β γ] [AddMonoidHomClass F β γ] (s : Finset α) (f : αβ) (comm : (s).Pairwise fun (a b : α) => AddCommute (f a) (f b)) (g : F) :
              g (s.noncommSum f comm) = s.noncommSum (fun (i : α) => g (f i))
              theorem Finset.map_noncommProd {F : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Monoid β] [Monoid γ] [FunLike F β γ] [MonoidHomClass F β γ] (s : Finset α) (f : αβ) (comm : (s).Pairwise fun (a b : α) => Commute (f a) (f b)) (g : F) :
              g (s.noncommProd f comm) = s.noncommProd (fun (i : α) => g (f i))
              @[deprecated Finset.map_noncommProd]
              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 : (s).Pairwise fun (a b : α) => Commute (f a) (f b)) (g : F) :
              g (s.noncommProd f comm) = s.noncommProd (fun (i : α) => g (f i))

              Alias of Finset.map_noncommProd.

              @[deprecated Finset.map_noncommSum]
              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 : (s).Pairwise fun (a b : α) => AddCommute (f a) (f b)) (g : F) :
              g (s.noncommSum f comm) = s.noncommSum (fun (i : α) => g (f i))

              Alias of Finset.map_noncommSum.

              theorem Finset.noncommSum_eq_card_nsmul {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (f : αβ) (comm : (s).Pairwise fun (a b : α) => AddCommute (f a) (f b)) (m : β) (h : xs, f x = m) :
              s.noncommSum f comm = s.card m
              theorem Finset.noncommProd_eq_pow_card {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (f : αβ) (comm : (s).Pairwise fun (a b : α) => Commute (f a) (f b)) (m : β) (h : xs, f x = m) :
              s.noncommProd f comm = m ^ s.card
              theorem Finset.noncommSum_addCommute {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (f : αβ) (comm : (s).Pairwise fun (a b : α) => AddCommute (f a) (f b)) (y : β) (h : xs, AddCommute y (f x)) :
              AddCommute y (s.noncommSum f comm)
              theorem Finset.noncommProd_commute {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (f : αβ) (comm : (s).Pairwise fun (a b : α) => Commute (f a) (f b)) (y : β) (h : xs, Commute y (f x)) :
              Commute y (s.noncommProd f comm)
              theorem Finset.mul_noncommProd_erase {α : Type u_3} {β : Type u_4} [Monoid β] [DecidableEq α] (s : Finset α) {a : α} (h : a s) (f : αβ) (comm : (s).Pairwise fun (a b : α) => Commute (f a) (f b)) (comm' : optParam (x(s.erase a), y(s.erase a), x y(fun (a b : α) => Commute (f a) (f b)) x y) ) :
              f a * (s.erase a).noncommProd f comm' = s.noncommProd f comm
              theorem Finset.noncommProd_erase_mul {α : Type u_3} {β : Type u_4} [Monoid β] [DecidableEq α] (s : Finset α) {a : α} (h : a s) (f : αβ) (comm : (s).Pairwise fun (a b : α) => Commute (f a) (f b)) (comm' : optParam (x(s.erase a), y(s.erase a), x y(fun (a b : α) => Commute (f a) (f b)) x y) ) :
              (s.erase a).noncommProd f comm' * f a = s.noncommProd f comm
              theorem Finset.noncommSum_eq_sum {α : Type u_3} {β : Type u_6} [AddCommMonoid β] (s : Finset α) (f : αβ) :
              s.noncommSum f = s.sum f
              theorem Finset.noncommProd_eq_prod {α : Type u_3} {β : Type u_6} [CommMonoid β] (s : Finset α) (f : αβ) :
              s.noncommProd f = s.prod 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 : {x : α | x s t}.Pairwise fun (a b : α) => AddCommute (f a) (f b)) :
              (s t).noncommSum f comm = s.noncommSum f + t.noncommSum f

              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 : {x : α | x s t}.Pairwise fun (a b : α) => Commute (f a) (f b)) :
              (s t).noncommProd f comm = s.noncommProd f * t.noncommProd f

              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 : (s).Pairwise fun (x y : α) => AddCommute (f x) (f y)) (comm_gg : (s).Pairwise fun (x y : α) => AddCommute (g x) (g y)) (comm_gf : (s).Pairwise fun (x y : α) => AddCommute (g x) (f y)) :
              (s).Pairwise 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 : (s).Pairwise fun (x y : α) => Commute (f x) (f y)) (comm_gg : (s).Pairwise fun (x y : α) => Commute (g x) (g y)) (comm_gf : (s).Pairwise fun (x y : α) => Commute (g x) (f y)) :
              (s).Pairwise 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 : (s).Pairwise fun (x y : α) => AddCommute (f x) (f y)) (comm_gg : (s).Pairwise fun (x y : α) => AddCommute (g x) (g y)) (comm_gf : (s).Pairwise fun (x y : α) => AddCommute (g x) (f y)) :
              s.noncommSum (f + g) = s.noncommSum f comm_ff + s.noncommSum g comm_gg

              The 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 : (s).Pairwise fun (x y : α) => Commute (f x) (f y)) (comm_gg : (s).Pairwise fun (x y : α) => Commute (g x) (g y)) (comm_gf : (s).Pairwise fun (x y : α) => Commute (g x) (f y)) :
              s.noncommProd (f * g) = s.noncommProd f comm_ff * s.noncommProd g comm_gg

              The 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.univ.noncommSum (fun (i : ι) => Pi.single i (x i)) = x
              theorem Finset.noncommProd_mul_single {ι : Type u_2} {M : ιType u_6} [(i : ι) → Monoid (M i)] [Fintype ι] [DecidableEq ι] (x : (i : ι) → M i) :
              Finset.univ.noncommProd (fun (i : ι) => Pi.mulSingle i (x i)) = 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