# 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.

Equations
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
@[protected]
theorem multiset.nocomm_sum_map_aux {α : Type u_1} {β : Type u_2} [add_monoid α] [add_monoid β] (s : multiset α) (comm : ∀ (x : α), x s∀ (y : α), y s y) {F : Type u_3} [ β] (f : F) (x : β) (H : x ) (y : β) (H_1 : y ) :
y
@[protected]
theorem multiset.nocomm_prod_map_aux {α : Type u_1} {β : Type u_2} [monoid α] [monoid β] (s : multiset α) (comm : ∀ (x : α), x s∀ (y : α), y s y) {F : Type u_3} [ β] (f : F) (x : β) (H : x ) (y : β) (H_1 : y ) :
y
theorem multiset.noncomm_prod_map {α : Type u_1} {β : Type u_2} [monoid α] [monoid β] (s : multiset α) (comm : ∀ (x : α), x s∀ (y : α), y s y) {F : Type u_3} [ β] (f : F) :
theorem multiset.noncomm_sum_map {α : Type u_1} {β : Type u_2} [add_monoid α] [add_monoid β] (s : multiset α) (comm : ∀ (x : α), x s∀ (y : α), y s y) {F : Type u_3} [ β] (f : F) :
f (s.noncomm_sum comm) = s).noncomm_sum _
theorem multiset.noncomm_prod_eq_pow_card {α : Type u_1} [monoid α] (s : multiset α) (comm : ∀ (x : α), x s∀ (y : α), y s y) (m : α) (h : ∀ (x : α), x sx = m) :
s.noncomm_prod comm =
theorem multiset.noncomm_sum_eq_card_nsmul {α : Type u_1} [add_monoid α] (s : multiset α) (comm : ∀ (x : α), x s∀ (y : α), y s y) (m : α) (h : ∀ (x : α), x sx = m) :
s.noncomm_sum comm =
theorem multiset.noncomm_sum_eq_sum {α : Type u_1} (s : multiset α) :
theorem multiset.noncomm_prod_eq_prod {α : Type u_1} [comm_monoid α] (s : multiset α) :
theorem multiset.noncomm_sum_add_commute {α : Type u_1} [add_monoid α] (s : multiset α) (comm : ∀ (x : α), x s∀ (y : α), y s y) (y : α) (h : ∀ (x : α), x s x) :
(s.noncomm_sum comm)
theorem multiset.noncomm_prod_commute {α : Type u_1} [monoid α] (s : multiset α) (comm : ∀ (x : α), x s∀ (y : α), y s y) (y : α) (h : ∀ (x : α), x s x) :
(s.noncomm_prod comm)
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.

Equations
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
theorem finset.noncomm_sum_congr {α : Type u_1} {β : Type u_2} [add_monoid β] {s₁ s₂ : finset α} {f g : α → β} (h₁ : s₁ = s₂) (h₂ : ∀ (x : α), x s₂f x = g x) (comm : ∀ (x : α), x s₁∀ (y : α), y s₁add_commute (f x) (f y)) :
s₁.noncomm_sum f comm = s₂.noncomm_sum g _
theorem finset.noncomm_prod_congr {α : Type u_1} {β : Type u_2} [monoid β] {s₁ s₂ : finset α} {f g : α → β} (h₁ : s₁ = s₂) (h₂ : ∀ (x : α), x s₂f x = g x) (comm : ∀ (x : α), x s₁∀ (y : α), y s₁commute (f x) (f y)) :
s₁.noncomm_prod f comm = s₂.noncomm_prod g _
@[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 ∀ (y : α), y add_commute (f x) (f y)) (ha : a s) :
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 ∀ (y : α), y commute (f x) (f y)) (ha : a s) :
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 ∀ (y : α), y add_commute (f x) (f y)) (ha : a s) :
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 ∀ (y : α), y commute (f x) (f y)) (ha : a s) :
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_sum_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_monoid β] [add_monoid γ] (s : finset α) (f : α → β) (comm : ∀ (x : α), x s∀ (y : α), y sadd_commute (f x) (f y)) {F : Type u_4} [ γ] (g : F) :
g (s.noncomm_sum f comm) = s.noncomm_sum (λ (i : α), g (f i)) _
theorem finset.noncomm_prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [monoid β] [monoid γ] (s : finset α) (f : α → β) (comm : ∀ (x : α), x s∀ (y : α), y scommute (f x) (f y)) {F : Type u_4} [ γ] (g : F) :
g (s.noncomm_prod f comm) = s.noncomm_prod (λ (i : α), g (f i)) _
theorem finset.noncomm_sum_eq_card_nsmul {α : Type u_1} {β : Type u_2} [add_monoid β] (s : finset α) (f : α → β) (comm : ∀ (x : α), x s∀ (y : α), y sadd_commute (f x) (f y)) (m : β) (h : ∀ (x : α), x sf x = m) :
s.noncomm_sum f comm = s.card m
theorem finset.noncomm_prod_eq_pow_card {α : Type u_1} {β : Type u_2} [monoid β] (s : finset α) (f : α → β) (comm : ∀ (x : α), x s∀ (y : α), y scommute (f x) (f y)) (m : β) (h : ∀ (x : α), x sf x = m) :
s.noncomm_prod f comm = m ^ s.card
theorem finset.noncomm_sum_add_commute {α : Type u_1} {β : Type u_2} [add_monoid β] (s : finset α) (f : α → β) (comm : ∀ (x : α), x s∀ (y : α), y sadd_commute (f x) (f y)) (y : β) (h : ∀ (x : α), x s (f x)) :
(s.noncomm_sum f comm)
theorem finset.noncomm_prod_commute {α : Type u_1} {β : Type u_2} [monoid β] (s : finset α) (f : α → β) (comm : ∀ (x : α), x s∀ (y : α), y scommute (f x) (f y)) (y : β) (h : ∀ (x : α), x s (f x)) :
(s.noncomm_prod f comm)
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
@[protected]
theorem finset.noncomm_prod_mul_distrib_aux {α : Type u_1} {β : Type u_2} [monoid β] {s : finset α} {f g : α → β} (comm_ff : ∀ (x : α), x s∀ (y : α), y scommute (f x) (f y)) (comm_gg : ∀ (x : α), x s∀ (y : α), y scommute (g x) (g y)) (comm_gf : ∀ (x : α), x s∀ (y : α), y sx ycommute (g x) (f y)) (x : α) (H : x s) (y : α) (H_1 : y s) :
commute ((f * g) x) ((f * g) y)
@[protected]
theorem finset.noncomm_sum_add_distrib_aux {α : Type u_1} {β : Type u_2} [add_monoid β] {s : finset α} {f g : α → β} (comm_ff : ∀ (x : α), x s∀ (y : α), y sadd_commute (f x) (f y)) (comm_gg : ∀ (x : α), x s∀ (y : α), y sadd_commute (g x) (g y)) (comm_gf : ∀ (x : α), x s∀ (y : α), y sx yadd_commute (g x) (f y)) (x : α) (H : x s) (y : α) (H_1 : y s) :
add_commute ((f + g) x) ((f + g) y)
theorem finset.noncomm_sum_add_distrib {α : Type u_1} {β : Type u_2} [add_monoid β] {s : finset α} (f g : α → β) (comm_ff : ∀ (x : α), x s∀ (y : α), y sadd_commute (f x) (f y)) (comm_gg : ∀ (x : α), x s∀ (y : α), y sadd_commute (g x) (g y)) (comm_gf : ∀ (x : α), x s∀ (y : α), y sx yadd_commute (g x) (f y)) :
s.noncomm_sum (f + g) _ = s.noncomm_sum f comm_ff + s.noncomm_sum g comm_gg

The non-commutative version of finset.sum_add_distrib

theorem finset.noncomm_prod_mul_distrib {α : Type u_1} {β : Type u_2} [monoid β] {s : finset α} (f g : α → β) (comm_ff : ∀ (x : α), x s∀ (y : α), y scommute (f x) (f y)) (comm_gg : ∀ (x : α), x s∀ (y : α), y scommute (g x) (g y)) (comm_gf : ∀ (x : α), x s∀ (y : α), y sx ycommute (g x) (f y)) :
s.noncomm_prod (f * g) _ = s.noncomm_prod f comm_ff * s.noncomm_prod g comm_gg

The non-commutative version of finset.prod_mul_distrib

theorem finset.noncomm_sum_single {ι : Type u_4} [fintype ι] [decidable_eq ι] {M : ι → Type u_5} [Π (i : ι), add_monoid (M i)] (x : Π (i : ι), M i) :
finset.univ.noncomm_sum (λ (i : ι), (x i)) _ = x
theorem finset.noncomm_prod_mul_single {ι : Type u_4} [fintype ι] [decidable_eq ι] {M : ι → Type u_5} [Π (i : ι), monoid (M i)] (x : Π (i : ι), M i) :
finset.univ.noncomm_prod (λ (i : ι), (x i)) _ = x
theorem add_monoid_hom.pi_ext {γ : Type u_3} [add_monoid γ] {ι : Type u_4} [fintype ι] [decidable_eq ι] {M : ι → Type u_5} [Π (i : ι), add_monoid (M i)] {f g : (Π (i : ι), M i) →+ γ} (h : ∀ (i : ι) (x : M i), f x) = g x)) :
f = g
theorem monoid_hom.pi_ext {γ : Type u_3} [monoid γ] {ι : Type u_4} [fintype ι] [decidable_eq ι] {M : ι → Type u_5} [Π (i : ι), monoid (M i)] {f g : (Π (i : ι), M i) →* γ} (h : ∀ (i : ι) (x : M i), f x) = g x)) :
f = g