# mathlib3documentation

data.finset.noncomm_prod

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_3} {β : Type u_4} (f : α β β) (s : multiset α) (comm : {x : α | x s}.pairwise (λ (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 left_commutative f on all elements x ∈ s.

Equations
@[simp]
theorem multiset.noncomm_foldr_coe {α : Type u_3} {β : Type u_4} (f : α β β) (l : list α) (comm : {x : α | x l}.pairwise (λ (x y : α), (b : β), f x (f y b) = f y (f x b))) (b : β) :
comm b = b l
@[simp]
theorem multiset.noncomm_foldr_empty {α : Type u_3} {β : Type u_4} (f : α β β) (h : {x : α | x 0}.pairwise (λ (x y : α), (b : β), f x (f y b) = f y (f x b))) (b : β) :
b = b
theorem multiset.noncomm_foldr_cons {α : Type u_3} {β : Type u_4} (f : α β β) (s : multiset α) (a : α) (h : {x : α | x a ::ₘ s}.pairwise (λ (x y : α), (b : β), f x (f y b) = f y (f x b))) (h' : {x : α | x s}.pairwise (λ (x y : α), (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_3} {β : Type u_4} (f : α β β) (s : multiset α) (h : left_commutative f) (b : β) :
b = b s
def multiset.noncomm_fold {α : Type u_3} (op : α α α) [assoc : op] (s : multiset α) (comm : {x : α | x s}.pairwise (λ (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
• comm = _
@[simp]
theorem multiset.noncomm_fold_coe {α : Type u_3} (op : α α α) [assoc : op] (l : list α) (comm : {x : α | x l}.pairwise (λ (x y : α), op x y = op y x)) (a : α) :
comm a = a l
@[simp]
theorem multiset.noncomm_fold_empty {α : Type u_3} (op : α α α) [assoc : op] (h : {x : α | x 0}.pairwise (λ (x y : α), op x y = op y x)) (a : α) :
h a = a
theorem multiset.noncomm_fold_cons {α : Type u_3} (op : α α α) [assoc : op] (s : multiset α) (a : α) (h : {x : α | x a ::ₘ s}.pairwise (λ (x y : α), op x y = op y x)) (h' : {x : α | x s}.pairwise (λ (x y : α), op x y = op y x)) (x : α) :
(a ::ₘ s) h x = op a h' x)
theorem multiset.noncomm_fold_eq_fold {α : Type u_3} (op : α α α) [assoc : op] (s : multiset α) [ op] (a : α) :
_ a = a s
def multiset.noncomm_sum {α : Type u_3} [add_monoid α] (s : multiset α) (comm : {x : α | x s}.pairwise add_commute) :
α

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_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
@[simp]
theorem multiset.noncomm_sum_coe {α : Type u_3} [add_monoid α] (l : list α) (comm : {x : α | x l}.pairwise add_commute) :
@[simp]
theorem multiset.noncomm_prod_coe {α : Type u_3} [monoid α] (l : list α) (comm : {x : α | x l}.pairwise commute) :
@[simp]
theorem multiset.noncomm_prod_empty {α : Type u_3} [monoid α] (h : {x : α | x 0}.pairwise commute) :
@[simp]
theorem multiset.noncomm_sum_empty {α : Type u_3} [add_monoid α] (h : {x : α | x 0}.pairwise add_commute) :
@[simp]
theorem multiset.noncomm_prod_cons {α : Type u_3} [monoid α] (s : multiset α) (a : α) (comm : {x : α | x a ::ₘ s}.pairwise commute) :
(a ::ₘ s).noncomm_prod comm = a * s.noncomm_prod _
@[simp]
theorem multiset.noncomm_sum_cons {α : Type u_3} [add_monoid α] (s : multiset α) (a : α) (comm : {x : α | x a ::ₘ s}.pairwise add_commute) :
(a ::ₘ s).noncomm_sum comm = a + s.noncomm_sum _
theorem multiset.noncomm_sum_cons' {α : Type u_3} [add_monoid α] (s : multiset α) (a : α) (comm : {x : α | x a ::ₘ s}.pairwise add_commute) :
(a ::ₘ s).noncomm_sum comm = s.noncomm_sum _ + a
theorem multiset.noncomm_prod_cons' {α : Type u_3} [monoid α] (s : multiset α) (a : α) (comm : {x : α | x a ::ₘ s}.pairwise commute) :
(a ::ₘ s).noncomm_prod comm = s.noncomm_prod _ * a
theorem multiset.noncomm_sum_add {α : Type u_3} [add_monoid α] (s t : multiset α) (comm : {x : α | x s + t}.pairwise add_commute) :
(s + t).noncomm_sum comm = s.noncomm_sum _ + t.noncomm_sum _
theorem multiset.noncomm_prod_add {α : Type u_3} [monoid α] (s t : multiset α) (comm : {x : α | x s + t}.pairwise commute) :
@[protected]
theorem multiset.noncomm_prod_map_aux {F : Type u_1} {α : Type u_3} {β : Type u_4} [monoid α] [monoid β] [ β] (s : multiset α) (comm : {x : α | x s}.pairwise commute) (f : F) :
{x : β | x s}.pairwise commute
@[protected]
theorem multiset.noncomm_sum_map_aux {F : Type u_1} {α : Type u_3} {β : Type u_4} [add_monoid α] [add_monoid β] [ β] (s : multiset α) (comm : {x : α | x s}.pairwise add_commute) (f : F) :
{x : β | x s}.pairwise add_commute
theorem multiset.noncomm_prod_map {F : Type u_1} {α : Type u_3} {β : Type u_4} [monoid α] [monoid β] [ β] (s : multiset α) (comm : {x : α | x s}.pairwise commute) (f : F) :
theorem multiset.noncomm_sum_map {F : Type u_1} {α : Type u_3} {β : Type u_4} [add_monoid α] [add_monoid β] [ β] (s : multiset α) (comm : {x : α | x s}.pairwise add_commute) (f : F) :
f (s.noncomm_sum comm) = s).noncomm_sum _
theorem multiset.noncomm_prod_eq_pow_card {α : Type u_3} [monoid α] (s : multiset α) (comm : {x : α | x s}.pairwise commute) (m : α) (h : (x : α), x s x = m) :
s.noncomm_prod comm =
theorem multiset.noncomm_sum_eq_card_nsmul {α : Type u_3} [add_monoid α] (s : multiset α) (comm : {x : α | x s}.pairwise add_commute) (m : α) (h : (x : α), x s x = 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_3} [add_monoid α] (s : multiset α) (comm : {x : α | x s}.pairwise add_commute) (y : α) (h : (x : α), x s x) :
(s.noncomm_sum comm)
theorem multiset.noncomm_prod_commute {α : Type u_3} [monoid α] (s : multiset α) (comm : {x : α | x s}.pairwise commute) (y : α) (h : (x : α), x s x) :
(s.noncomm_prod comm)
def finset.noncomm_sum {α : Type u_3} {β : Type u_4} [add_monoid β] (s : finset α) (f : α β) (comm : s.pairwise (λ (a b : α), add_commute (f a) (f b))) :
β

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_3} {β : Type u_4} [monoid β] (s : finset α) (f : α β) (comm : s.pairwise (λ (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.noncomm_sum_congr {α : Type u_3} {β : Type u_4} [add_monoid β] {s₁ s₂ : finset α} {f g : α β} (h₁ : s₁ = s₂) (h₂ : (x : α), x s₂ f x = g x) (comm : s₁.pairwise (λ (a b : α), add_commute (f a) (f b))) :
s₁.noncomm_sum f comm = s₂.noncomm_sum g _
theorem finset.noncomm_prod_congr {α : Type u_3} {β : Type u_4} [monoid β] {s₁ s₂ : finset α} {f g : α β} (h₁ : s₁ = s₂) (h₂ : (x : α), x s₂ f x = g x) (comm : s₁.pairwise (λ (a b : α), commute (f a) (f b))) :
s₁.noncomm_prod f comm = s₂.noncomm_prod g _
@[simp]
theorem finset.noncomm_prod_to_finset {α : Type u_3} {β : Type u_4} [monoid β] [decidable_eq α] (l : list α) (f : α β) (comm : (l.to_finset).pairwise (λ (a b : α), commute (f a) (f b))) (hl : l.nodup) :
comm = (list.map f l).prod
@[simp]
theorem finset.noncomm_sum_to_finset {α : Type u_3} {β : Type u_4} [add_monoid β] [decidable_eq α] (l : list α) (f : α β) (comm : (l.to_finset).pairwise (λ (a b : α), add_commute (f a) (f b))) (hl : l.nodup) :
comm = (list.map f l).sum
@[simp]
theorem finset.noncomm_prod_empty {α : Type u_3} {β : Type u_4} [monoid β] (f : α β) (h : .pairwise (λ (a b : α), commute (f a) (f b))) :
h = 1
@[simp]
theorem finset.noncomm_sum_empty {α : Type u_3} {β : Type u_4} [add_monoid β] (f : α β) (h : .pairwise (λ (a b : α), add_commute (f a) (f b))) :
h = 0
@[simp]
theorem finset.noncomm_sum_insert_of_not_mem {α : Type u_3} {β : Type u_4} [add_monoid β] [decidable_eq α] (s : finset α) (a : α) (f : α β) (comm : s).pairwise (λ (a b : α), add_commute (f a) (f b))) (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_3} {β : Type u_4} [monoid β] [decidable_eq α] (s : finset α) (a : α) (f : α β) (comm : s).pairwise (λ (a b : α), commute (f a) (f b))) (ha : a s) :
f comm = f a * s.noncomm_prod f _
theorem finset.noncomm_sum_insert_of_not_mem' {α : Type u_3} {β : Type u_4} [add_monoid β] [decidable_eq α] (s : finset α) (a : α) (f : α β) (comm : s).pairwise (λ (a b : α), add_commute (f a) (f b))) (ha : a s) :
s).noncomm_sum f comm = s.noncomm_sum f _ + f a
theorem finset.noncomm_prod_insert_of_not_mem' {α : Type u_3} {β : Type u_4} [monoid β] [decidable_eq α] (s : finset α) (a : α) (f : α β) (comm : s).pairwise (λ (a b : α), commute (f a) (f b))) (ha : a s) :
f comm = s.noncomm_prod f _ * f a
@[simp]
theorem finset.noncomm_prod_singleton {α : Type u_3} {β : Type u_4} [monoid β] (a : α) (f : α β) :
{a}.noncomm_prod f _ = f a
@[simp]
theorem finset.noncomm_sum_singleton {α : Type u_3} {β : Type u_4} [add_monoid β] (a : α) (f : α β) :
{a}.noncomm_sum f _ = f a
theorem finset.noncomm_sum_map {F : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [add_monoid β] [add_monoid γ] [ γ] (s : finset α) (f : α β) (comm : s.pairwise (λ (a b : α), add_commute (f a) (f b))) (g : F) :
g (s.noncomm_sum f comm) = s.noncomm_sum (λ (i : α), g (f i)) _
theorem finset.noncomm_prod_map {F : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [monoid β] [monoid γ] [ γ] (s : finset α) (f : α β) (comm : s.pairwise (λ (a b : α), commute (f a) (f b))) (g : F) :
g (s.noncomm_prod f comm) = s.noncomm_prod (λ (i : α), g (f i)) _
theorem finset.noncomm_sum_eq_card_nsmul {α : Type u_3} {β : Type u_4} [add_monoid β] (s : finset α) (f : α β) (comm : s.pairwise (λ (a b : α), add_commute (f a) (f b))) (m : β) (h : (x : α), x s f x = m) :
s.noncomm_sum f comm = s.card m
theorem finset.noncomm_prod_eq_pow_card {α : Type u_3} {β : Type u_4} [monoid β] (s : finset α) (f : α β) (comm : s.pairwise (λ (a b : α), commute (f a) (f b))) (m : β) (h : (x : α), x s f x = m) :
s.noncomm_prod f comm = m ^ s.card
theorem finset.noncomm_sum_add_commute {α : Type u_3} {β : Type u_4} [add_monoid β] (s : finset α) (f : α β) (comm : s.pairwise (λ (a b : α), add_commute (f a) (f b))) (y : β) (h : (x : α), x s (f x)) :
(s.noncomm_sum f comm)
theorem finset.noncomm_prod_commute {α : Type u_3} {β : Type u_4} [monoid β] (s : finset α) (f : α β) (comm : s.pairwise (λ (a b : α), commute (f a) (f b))) (y : β) (h : (x : α), x s (f x)) :
(s.noncomm_prod f comm)
theorem finset.noncomm_prod_eq_prod {α : Type u_3} {β : Type u_1} [comm_monoid β] (s : finset α) (f : α β) :
s.noncomm_prod f _ = s.prod f
theorem finset.noncomm_sum_eq_sum {α : Type u_3} {β : Type u_1} (s : finset α) (f : α β) :
s.noncomm_sum f _ = s.sum f
theorem finset.noncomm_sum_union_of_disjoint {α : Type u_3} {β : Type u_4} [add_monoid β] [decidable_eq α] {s t : finset α} (h : t) (f : α β) (comm : {x : α | x s t}.pairwise (λ (a b : α), add_commute (f a) (f b))) :
(s t).noncomm_sum f comm = s.noncomm_sum f _ + t.noncomm_sum f _

The non-commutative version of finset.sum_union

theorem finset.noncomm_prod_union_of_disjoint {α : Type u_3} {β : Type u_4} [monoid β] [decidable_eq α] {s t : finset α} (h : t) (f : α β) (comm : {x : α | x s t}.pairwise (λ (a b : α), commute (f a) (f b))) :
(s t).noncomm_prod f comm = s.noncomm_prod f _ * t.noncomm_prod f _

The non-commutative version of finset.prod_union

@[protected]
theorem finset.noncomm_prod_mul_distrib_aux {α : Type u_3} {β : Type u_4} [monoid β] {s : finset α} {f g : α β} (comm_ff : s.pairwise (λ (x y : α), commute (f x) (f y))) (comm_gg : s.pairwise (λ (x y : α), commute (g x) (g y))) (comm_gf : s.pairwise (λ (x y : α), commute (g x) (f y))) :
s.pairwise (λ (x y : α), commute ((f * g) x) ((f * g) y))
@[protected]
theorem finset.noncomm_sum_add_distrib_aux {α : Type u_3} {β : Type u_4} [add_monoid β] {s : finset α} {f g : α β} (comm_ff : s.pairwise (λ (x y : α), add_commute (f x) (f y))) (comm_gg : s.pairwise (λ (x y : α), add_commute (g x) (g y))) (comm_gf : s.pairwise (λ (x y : α), add_commute (g x) (f y))) :
s.pairwise (λ (x y : α), add_commute ((f + g) x) ((f + g) y))
theorem finset.noncomm_sum_add_distrib {α : Type u_3} {β : Type u_4} [add_monoid β] {s : finset α} (f g : α β) (comm_ff : s.pairwise (λ (x y : α), add_commute (f x) (f y))) (comm_gg : s.pairwise (λ (x y : α), add_commute (g x) (g y))) (comm_gf : s.pairwise (λ (x y : α), add_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_3} {β : Type u_4} [monoid β] {s : finset α} (f g : α β) (comm_ff : s.pairwise (λ (x y : α), commute (f x) (f y))) (comm_gg : s.pairwise (λ (x y : α), commute (g x) (g y))) (comm_gf : s.pairwise (λ (x y : α), commute (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_2} {M : ι Type u_6} [Π (i : ι), add_monoid (M i)] [fintype ι] [decidable_eq ι] (x : Π (i : ι), M i) :
finset.univ.noncomm_sum (λ (i : ι), (x i)) _ = x
theorem finset.noncomm_prod_mul_single {ι : Type u_2} {M : ι Type u_6} [Π (i : ι), monoid (M i)] [fintype ι] [decidable_eq ι] (x : Π (i : ι), M i) :
finset.univ.noncomm_prod (λ (i : ι), (x i)) _ = x
theorem add_monoid_hom.pi_ext {ι : Type u_2} {γ : Type u_5} [add_monoid γ] {M : ι Type u_6} [Π (i : ι), add_monoid (M i)] [finite ι] [decidable_eq ι] {f g : (Π (i : ι), M i) →+ γ} (h : (i : ι) (x : M i), f x) = g x)) :
f = g
theorem monoid_hom.pi_ext {ι : Type u_2} {γ : Type u_5} [monoid γ] {M : ι Type u_6} [Π (i : ι), monoid (M i)] [finite ι] [decidable_eq ι] {f g : (Π (i : ι), M i) →* γ} (h : (i : ι) (x : M i), f x) = g x)) :
f = g