# mathlibdocumentation

data.finset.noncomm_prod

# Products (respectively, sums) over a finset or a multiset. #

The regular finset.prod and multiset.prod require [comm_monoid α]. 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.noncomm_prod, requiring a proof of commutativity of held terms
• multiset.noncomm_prod, requiring a proof of commutativity of held terms

## Implementation details #

While list.prod is defined via list.foldl, noncomm_prod is defined via multiset.foldr for neater proofs and definitions. By the commutativity assumption, the two must be equal.

def multiset.noncomm_foldr {α : Type u_1} {β : Type u_2} (f : α → β → β) (s : multiset α) (comm : ∀ (x : α), x s∀ (y : α), y s∀ (b : β), f x (f y b) = f y (f x b)) (b : β) :
β

Fold of a s : multiset α with f : α → β → β, given a proof that left_commutative f on all elements x ∈ s.

Equations
@[simp]
theorem multiset.noncomm_foldr_coe {α : Type u_1} {β : Type u_2} (f : α → β → β) (l : list α) (comm : ∀ (x : α), x l∀ (y : α), y l∀ (b : β), f x (f y b) = f y (f x b)) (b : β) :
comm b = b l
@[simp]
theorem multiset.noncomm_foldr_empty {α : Type u_1} {β : Type u_2} (f : α → β → β) (h : ∀ (x : α), x 0∀ (y : α), y 0∀ (b : β), f x (f y b) = f y (f x b)) (b : β) :
b = b
theorem multiset.noncomm_foldr_cons {α : Type u_1} {β : Type u_2} (f : α → β → β) (s : multiset α) (a : α) (h : ∀ (x : α), x a ::ₘ s∀ (y : α), y a ::ₘ s∀ (b : β), f x (f y b) = f y (f x b)) (h' : ∀ (x : α), x s∀ (y : α), y s∀ (b : β), f x (f y b) = f y (f x b)) (b : β) :
(a ::ₘ s) h b = f a h' b)
theorem multiset.noncomm_foldr_eq_foldr {α : Type u_1} {β : Type u_2} (f : α → β → β) (s : multiset α) (h : left_commutative f) (b : β) :
b = b s
def multiset.noncomm_fold {α : Type u_1} (op : α → α → α) [assoc : op] (s : multiset α) (comm : ∀ (x : α), x s∀ (y : α), y sop x y = op y x) (a : α) :
α

Fold of a s : multiset α with an associative op : α → α → α, given a proofs that op is commutative on all elements x ∈ s.

Equations
• comm a = _ a
@[simp]
theorem multiset.noncomm_fold_coe {α : Type u_1} (op : α → α → α) [assoc : op] (l : list α) (comm : ∀ (x : α), x l∀ (y : α), y lop x y = op y x) (a : α) :
comm a = a l
@[simp]
theorem multiset.noncomm_fold_empty {α : Type u_1} (op : α → α → α) [assoc : op] (h : ∀ (x : α), x 0∀ (y : α), y 0op x y = op y x) (a : α) :
h a = a
theorem multiset.noncomm_fold_cons {α : Type u_1} (op : α → α → α) [assoc : op] (s : multiset α) (a : α) (h : ∀ (x : α), x a ::ₘ s∀ (y : α), y a ::ₘ sop x y = op y x) (h' : ∀ (x : α), x s∀ (y : α), y sop x y = op y x) (x : α) :
(a ::ₘ s) h x = op a h' x)
theorem multiset.noncomm_fold_eq_fold {α : Type u_1} (op : α → α → α) [assoc : op] (s : multiset α) [ op] (a : α) :
_ a = a s
def multiset.noncomm_sum {α : Type u_1} [add_monoid α] (s : multiset α) (comm : ∀ (x : α), x s∀ (y : α), y s y) :
α

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

def multiset.noncomm_prod {α : Type u_1} [monoid α] (s : multiset α) (comm : ∀ (x : α), x s∀ (y : α), y s y) :
α

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

Equations
@[simp]
theorem multiset.noncomm_sum_coe {α : Type u_1} [add_monoid α] (l : list α) (comm : ∀ (x : α), x l∀ (y : α), y l y) :
@[simp]
theorem multiset.noncomm_prod_coe {α : Type u_1} [monoid α] (l : list α) (comm : ∀ (x : α), x l∀ (y : α), y l y) :
@[simp]
theorem multiset.noncomm_prod_empty {α : Type u_1} [monoid α] (h : ∀ (x : α), x 0∀ (y : α), y 0 y) :
@[simp]
theorem multiset.noncomm_sum_empty {α : Type u_1} [add_monoid α] (h : ∀ (x : α), x 0∀ (y : α), y 0 y) :
@[simp]
theorem multiset.noncomm_prod_cons {α : Type u_1} [monoid α] (s : multiset α) (a : α) (comm : ∀ (x : α), x a ::ₘ s∀ (y : α), y a ::ₘ s y) :
(a ::ₘ s).noncomm_prod comm = a * s.noncomm_prod _
@[simp]
theorem multiset.noncomm_sum_cons {α : Type u_1} [add_monoid α] (s : multiset α) (a : α) (comm : ∀ (x : α), x a ::ₘ s∀ (y : α), y a ::ₘ s y) :
(a ::ₘ s).noncomm_sum comm = a + s.noncomm_sum _
theorem multiset.noncomm_sum_cons' {α : Type u_1} [add_monoid α] (s : multiset α) (a : α) (comm : ∀ (x : α), x a ::ₘ s∀ (y : α), y a ::ₘ s y) :
(a ::ₘ s).noncomm_sum comm = s.noncomm_sum _ + a
theorem multiset.noncomm_prod_cons' {α : Type u_1} [monoid α] (s : multiset α) (a : α) (comm : ∀ (x : α), x a ::ₘ s∀ (y : α), y a ::ₘ s y) :
(a ::ₘ s).noncomm_prod comm = (s.noncomm_prod _) * a
theorem multiset.noncomm_sum_eq_sum {α : Type u_1} (s : multiset α) :
theorem multiset.noncomm_prod_eq_prod {α : Type u_1} [comm_monoid α] (s : multiset α) :
def finset.noncomm_sum {α : Type u_1} {β : Type u_2} [add_monoid β] (s : finset α) (f : α → β) (comm : ∀ (x : α), x s∀ (y : α), y sadd_commute (f x) (f y)) :
β

Sum of a s : finset α mapped with f : α → β with [add_monoid β], given a proof that + commutes on all elements f x for x ∈ s.

def finset.noncomm_prod {α : Type u_1} {β : Type u_2} [monoid β] (s : finset α) (f : α → β) (comm : ∀ (x : α), x s∀ (y : α), y scommute (f x) (f y)) :
β

Product of a s : finset α mapped with f : α → β with [monoid β], given a proof that * commutes on all elements f x for x ∈ s.

Equations
@[simp]
theorem finset.noncomm_prod_to_finset {α : Type u_1} {β : Type u_2} [monoid β] [decidable_eq α] (l : list α) (f : α → β) (comm : ∀ (x : α), x l.to_finset∀ (y : α), y l.to_finsetcommute (f x) (f y)) (hl : l.nodup) :
comm = (list.map f l).prod
@[simp]
theorem finset.noncomm_sum_to_finset {α : Type u_1} {β : Type u_2} [add_monoid β] [decidable_eq α] (l : list α) (f : α → β) (comm : ∀ (x : α), x l.to_finset∀ (y : α), y l.to_finsetadd_commute (f x) (f y)) (hl : l.nodup) :
comm = (list.map f l).sum
@[simp]
theorem finset.noncomm_prod_empty {α : Type u_1} {β : Type u_2} [monoid β] (f : α → β) (h : ∀ (x : α), x ∀ (y : α), y commute (f x) (f y)) :
h = 1
@[simp]
theorem finset.noncomm_sum_empty {α : Type u_1} {β : Type u_2} [add_monoid β] (f : α → β) (h : ∀ (x : α), x ∀ (y : α), y add_commute (f x) (f y)) :
h = 0
@[simp]
theorem finset.noncomm_sum_insert_of_not_mem {α : Type u_1} {β : Type u_2} [add_monoid β] [decidable_eq α] (s : finset α) (a : α) (f : α → β) (comm : ∀ (x : α), x s∀ (y : α), y sadd_commute (f x) (f y)) (ha : a s) :
(insert a s).noncomm_sum f comm = f a + s.noncomm_sum f _
@[simp]
theorem finset.noncomm_prod_insert_of_not_mem {α : Type u_1} {β : Type u_2} [monoid β] [decidable_eq α] (s : finset α) (a : α) (f : α → β) (comm : ∀ (x : α), x s∀ (y : α), y scommute (f x) (f y)) (ha : a s) :
(insert a s).noncomm_prod f comm = (f a) * s.noncomm_prod f _
theorem finset.noncomm_sum_insert_of_not_mem' {α : Type u_1} {β : Type u_2} [add_monoid β] [decidable_eq α] (s : finset α) (a : α) (f : α → β) (comm : ∀ (x : α), x s∀ (y : α), y sadd_commute (f x) (f y)) (ha : a s) :
(insert a s).noncomm_sum f comm = s.noncomm_sum f _ + f a
theorem finset.noncomm_prod_insert_of_not_mem' {α : Type u_1} {β : Type u_2} [monoid β] [decidable_eq α] (s : finset α) (a : α) (f : α → β) (comm : ∀ (x : α), x s∀ (y : α), y scommute (f x) (f y)) (ha : a s) :
(insert a s).noncomm_prod f comm = (s.noncomm_prod f _) * f a
@[simp]
theorem finset.noncomm_prod_singleton {α : Type u_1} {β : Type u_2} [monoid β] (a : α) (f : α → β) :
{a}.noncomm_prod f _ = f a
@[simp]
theorem finset.noncomm_sum_singleton {α : Type u_1} {β : Type u_2} [add_monoid β] (a : α) (f : α → β) :
{a}.noncomm_sum f _ = f a
theorem finset.noncomm_prod_eq_prod {α : Type u_1} {β : Type u_2} [comm_monoid β] (s : finset α) (f : α → β) :
s.noncomm_prod f _ = s.prod f
theorem finset.noncomm_sum_eq_sum {α : Type u_1} {β : Type u_2} (s : finset α) (f : α → β) :
s.noncomm_sum f _ = s.sum f
theorem finset.noncomm_sum_union_of_disjoint {α : Type u_1} {β : Type u_2} [add_monoid β] [decidable_eq α] {s t : finset α} (h : t) (f : α → β) (comm : ∀ (x : α), x s t∀ (y : α), y s tadd_commute (f x) (f y)) (scomm : (∀ (x : α), x s∀ (y : α), y sadd_commute (f x) (f y)) := _) (tcomm : (∀ (x : α), x t∀ (y : α), y tadd_commute (f x) (f y)) := _) :
(s t).noncomm_sum f comm = s.noncomm_sum f scomm + t.noncomm_sum f tcomm

The non-commutative version of finset.sum_union

theorem finset.noncomm_prod_union_of_disjoint {α : Type u_1} {β : Type u_2} [monoid β] [decidable_eq α] {s t : finset α} (h : t) (f : α → β) (comm : ∀ (x : α), x s t∀ (y : α), y s tcommute (f x) (f y)) (scomm : (∀ (x : α), x s∀ (y : α), y scommute (f x) (f y)) := _) (tcomm : (∀ (x : α), x t∀ (y : α), y tcommute (f x) (f y)) := _) :
(s t).noncomm_prod f comm = (s.noncomm_prod f scomm) * t.noncomm_prod f tcomm