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 termsmultiset.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
- multiset.noncomm_foldr f s comm b = multiset.foldr (f ∘ subtype.val) _ b s.attach
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 : β) :
multiset.noncomm_foldr f (a ::ₘ s) h b = f a (multiset.noncomm_foldr f s h' b)
theorem
multiset.noncomm_foldr_eq_foldr
{α : Type u_3}
{β : Type u_4}
(f : α → β → β)
(s : multiset α)
(h : left_commutative f)
(b : β) :
multiset.noncomm_foldr f s _ b = multiset.foldr f h b s
def
multiset.noncomm_fold
{α : Type u_3}
(op : α → α → α)
[assoc : is_associative α 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
- multiset.noncomm_fold op s comm = multiset.noncomm_foldr op s _
@[simp]
theorem
multiset.noncomm_fold_coe
{α : Type u_3}
(op : α → α → α)
[assoc : is_associative α op]
(l : list α)
(comm : {x : α | x ∈ ↑l}.pairwise (λ (x y : α), op x y = op y x))
(a : α) :
multiset.noncomm_fold op ↑l comm a = list.foldr op a l
@[simp]
theorem
multiset.noncomm_fold_empty
{α : Type u_3}
(op : α → α → α)
[assoc : is_associative α op]
(h : {x : α | x ∈ 0}.pairwise (λ (x y : α), op x y = op y x))
(a : α) :
multiset.noncomm_fold op 0 h a = a
theorem
multiset.noncomm_fold_cons
{α : Type u_3}
(op : α → α → α)
[assoc : is_associative α 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 : α) :
multiset.noncomm_fold op (a ::ₘ s) h x = op a (multiset.noncomm_fold op s h' x)
theorem
multiset.noncomm_fold_eq_fold
{α : Type u_3}
(op : α → α → α)
[assoc : is_associative α op]
(s : multiset α)
[is_commutative α op]
(a : α) :
multiset.noncomm_fold op s _ a = multiset.fold op 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
- s.noncomm_sum comm = multiset.noncomm_fold has_add.add s comm 0
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
- s.noncomm_prod comm = multiset.noncomm_fold has_mul.mul s comm 1
@[simp]
theorem
multiset.noncomm_sum_coe
{α : Type u_3}
[add_monoid α]
(l : list α)
(comm : {x : α | x ∈ ↑l}.pairwise add_commute) :
↑l.noncomm_sum comm = l.sum
@[simp]
theorem
multiset.noncomm_prod_empty
{α : Type u_3}
[monoid α]
(h : {x : α | x ∈ 0}.pairwise commute) :
0.noncomm_prod h = 1
@[simp]
theorem
multiset.noncomm_sum_empty
{α : Type u_3}
[add_monoid α]
(h : {x : α | x ∈ 0}.pairwise add_commute) :
0.noncomm_sum h = 0
@[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) :
(s + t).noncomm_prod comm = s.noncomm_prod _ * t.noncomm_prod _
@[protected]
theorem
multiset.noncomm_sum_map_aux
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[add_monoid α]
[add_monoid β]
[add_monoid_hom_class F α β]
(s : multiset α)
(comm : {x : α | x ∈ s}.pairwise add_commute)
(f : F) :
{x : β | x ∈ multiset.map ⇑f s}.pairwise add_commute
theorem
multiset.noncomm_prod_map
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[monoid α]
[monoid β]
[monoid_hom_class F α β]
(s : multiset α)
(comm : {x : α | x ∈ s}.pairwise commute)
(f : F) :
⇑f (s.noncomm_prod comm) = (multiset.map ⇑f s).noncomm_prod _
theorem
multiset.noncomm_sum_map
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[add_monoid α]
[add_monoid β]
[add_monoid_hom_class F α β]
(s : multiset α)
(comm : {x : α | x ∈ s}.pairwise add_commute)
(f : F) :
⇑f (s.noncomm_sum comm) = (multiset.map ⇑f s).noncomm_sum _
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 = ⇑multiset.card s • m
theorem
multiset.noncomm_sum_eq_sum
{α : Type u_1}
[add_comm_monoid α]
(s : multiset α) :
s.noncomm_sum _ = s.sum
theorem
multiset.noncomm_prod_eq_prod
{α : Type u_1}
[comm_monoid α]
(s : multiset α) :
s.noncomm_prod _ = s.prod
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 → add_commute y x) :
add_commute y (s.noncomm_sum 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
- s.noncomm_sum f comm = (multiset.map f s.val).noncomm_sum _
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
- s.noncomm_prod f comm = (multiset.map f s.val).noncomm_prod _
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 _
@[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) :
l.to_finset.noncomm_sum f comm = (list.map f l).sum
@[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))) :
∅.noncomm_sum f 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 : ↑(has_insert.insert a s).pairwise (λ (a b : α), add_commute (f a) (f b)))
(ha : a ∉ s) :
(has_insert.insert a 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 : ↑(has_insert.insert a s).pairwise (λ (a b : α), commute (f a) (f b)))
(ha : a ∉ s) :
(has_insert.insert a s).noncomm_prod 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 : ↑(has_insert.insert a s).pairwise (λ (a b : α), add_commute (f a) (f b)))
(ha : a ∉ s) :
(has_insert.insert a 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 : ↑(has_insert.insert a s).pairwise (λ (a b : α), commute (f a) (f b)))
(ha : a ∉ s) :
(has_insert.insert a s).noncomm_prod 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 γ]
[add_monoid_hom_class F β γ]
(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 γ]
[monoid_hom_class F β γ]
(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_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 → add_commute y (f x)) :
add_commute y (s.noncomm_sum 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}
[add_comm_monoid β]
(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 : disjoint s 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 : disjoint s 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]
@[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 : ι), pi.single 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 : ι), pi.mul_single 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 (pi.single i x) = ⇑g (pi.single i 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 (pi.mul_single i x) = ⇑g (pi.mul_single i x)) :
f = g