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 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_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
- multiset.noncomm_foldr f s comm b = multiset.foldr (f ∘ subtype.val) _ b s.attach
@[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 : β) :
multiset.noncomm_foldr f ↑l comm b = list.foldr f 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 : β) :
multiset.noncomm_foldr f 0 h 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 : β) :
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_1}
{β : Type u_2}
(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_1}
(op : α → α → α)
[assoc : is_associative α op]
(s : multiset α)
(comm : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → op 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
- multiset.noncomm_fold op s comm a = multiset.noncomm_foldr op s _ a
@[simp]
theorem
multiset.noncomm_fold_coe
{α : Type u_1}
(op : α → α → α)
[assoc : is_associative α op]
(l : list α)
(comm : ∀ (x : α), x ∈ ↑l → ∀ (y : α), y ∈ ↑l → 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_1}
(op : α → α → α)
[assoc : is_associative α op]
(h : ∀ (x : α), x ∈ 0 → ∀ (y : α), y ∈ 0 → op x y = op y x)
(a : α) :
multiset.noncomm_fold op 0 h a = a
theorem
multiset.noncomm_fold_cons
{α : Type u_1}
(op : α → α → α)
[assoc : is_associative α op]
(s : multiset α)
(a : α)
(h : ∀ (x : α), x ∈ a ::ₘ s → ∀ (y : α), y ∈ a ::ₘ s → op x y = op y x)
(h' : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → 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_1}
(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_1}
[add_monoid α]
(s : multiset α)
(comm : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → add_commute x y) :
α
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_1}
[monoid α]
(s : multiset α)
(comm : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → commute x y) :
α
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_1}
[add_monoid α]
(l : list α)
(comm : ∀ (x : α), x ∈ ↑l → ∀ (y : α), y ∈ ↑l → add_commute x y) :
↑l.noncomm_sum comm = l.sum
@[simp]
theorem
multiset.noncomm_prod_empty
{α : Type u_1}
[monoid α]
(h : ∀ (x : α), x ∈ 0 → ∀ (y : α), y ∈ 0 → commute x y) :
0.noncomm_prod h = 1
@[simp]
theorem
multiset.noncomm_sum_empty
{α : Type u_1}
[add_monoid α]
(h : ∀ (x : α), x ∈ 0 → ∀ (y : α), y ∈ 0 → add_commute x y) :
0.noncomm_sum h = 0
@[simp]
theorem
multiset.noncomm_prod_cons
{α : Type u_1}
[monoid α]
(s : multiset α)
(a : α)
(comm : ∀ (x : α), x ∈ a ::ₘ s → ∀ (y : α), y ∈ a ::ₘ s → commute x 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 → add_commute x 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 → add_commute x 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 → commute x 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 → add_commute x y)
{F : Type u_3}
[add_monoid_hom_class F α β]
(f : F)
(x : β)
(H : x ∈ multiset.map ⇑f s)
(y : β)
(H_1 : y ∈ multiset.map ⇑f s) :
add_commute x 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 → commute x y)
{F : Type u_3}
[monoid_hom_class F α β]
(f : F)
(x : β)
(H : x ∈ multiset.map ⇑f s)
(y : β)
(H_1 : y ∈ multiset.map ⇑f s) :
commute x y
theorem
multiset.noncomm_prod_map
{α : Type u_1}
{β : Type u_2}
[monoid α]
[monoid β]
(s : multiset α)
(comm : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → commute x y)
{F : Type u_3}
[monoid_hom_class F α β]
(f : F) :
⇑f (s.noncomm_prod comm) = (multiset.map ⇑f s).noncomm_prod _
theorem
multiset.noncomm_sum_map
{α : Type u_1}
{β : Type u_2}
[add_monoid α]
[add_monoid β]
(s : multiset α)
(comm : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → add_commute x y)
{F : Type u_3}
[add_monoid_hom_class F α β]
(f : F) :
⇑f (s.noncomm_sum comm) = (multiset.map ⇑f s).noncomm_sum _
theorem
multiset.noncomm_prod_eq_pow_card
{α : Type u_1}
[monoid α]
(s : multiset α)
(comm : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → commute x y)
(m : α)
(h : ∀ (x : α), x ∈ s → x = m) :
s.noncomm_prod comm = m ^ ⇑multiset.card s
theorem
multiset.noncomm_sum_eq_card_nsmul
{α : Type u_1}
[add_monoid α]
(s : multiset α)
(comm : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → add_commute x y)
(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_1}
[add_monoid α]
(s : multiset α)
(comm : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → add_commute x y)
(y : α)
(h : ∀ (x : α), x ∈ s → add_commute y x) :
add_commute y (s.noncomm_sum comm)
def
finset.noncomm_sum
{α : Type u_1}
{β : Type u_2}
[add_monoid β]
(s : finset α)
(f : α → β)
(comm : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → add_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
- s.noncomm_sum f comm = (multiset.map f s.val).noncomm_sum _
def
finset.noncomm_prod
{α : Type u_1}
{β : Type u_2}
[monoid β]
(s : finset α)
(f : α → β)
(comm : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → commute (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
- s.noncomm_prod f comm = (multiset.map f s.val).noncomm_prod _
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_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_finset → add_commute (f x) (f y))
(hl : l.nodup) :
l.to_finset.noncomm_sum f comm = (list.map f l).sum
@[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)) :
∅.noncomm_sum f 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 ∈ insert a s → ∀ (y : α), y ∈ insert a s → add_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 ∈ insert a s → ∀ (y : α), y ∈ insert a s → commute (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 ∈ insert a s → ∀ (y : α), y ∈ insert a s → add_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 ∈ insert a s → ∀ (y : α), y ∈ insert a s → commute (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_sum_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_monoid β]
[add_monoid γ]
(s : finset α)
(f : α → β)
(comm : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → add_commute (f x) (f y))
{F : Type u_4}
[add_monoid_hom_class F β γ]
(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 ∈ s → commute (f x) (f y))
{F : Type u_4}
[monoid_hom_class F β γ]
(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 ∈ s → add_commute (f x) (f y))
(m : β)
(h : ∀ (x : α), x ∈ s → f x = m) :
s.noncomm_sum f comm = s.card • m
theorem
finset.noncomm_sum_add_commute
{α : Type u_1}
{β : Type u_2}
[add_monoid β]
(s : finset α)
(f : α → β)
(comm : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → add_commute (f x) (f y))
(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_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}
[add_comm_monoid β]
(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 : disjoint s t)
(f : α → β)
(comm : ∀ (x : α), x ∈ s ∪ t → ∀ (y : α), y ∈ s ∪ t → add_commute (f x) (f y))
(scomm : (∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → add_commute (f x) (f y)) := _)
(tcomm : (∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → add_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 : disjoint s t)
(f : α → β)
(comm : ∀ (x : α), x ∈ s ∪ t → ∀ (y : α), y ∈ s ∪ t → commute (f x) (f y))
(scomm : (∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → commute (f x) (f y)) := _)
(tcomm : (∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → commute (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 ∈ s → commute (f x) (f y))
(comm_gg : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → commute (g x) (g y))
(comm_gf : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → commute (g x) (f y))
(x : α)
(H : x ∈ s)
(y : α)
(H_1 : y ∈ s) :
@[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 ∈ s → add_commute (f x) (f y))
(comm_gg : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → add_commute (g x) (g y))
(comm_gf : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → add_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 ∈ s → add_commute (f x) (f y))
(comm_gg : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → add_commute (g x) (g y))
(comm_gf : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → 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_1}
{β : Type u_2}
[monoid β]
{s : finset α}
(f g : α → β)
(comm_ff : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → commute (f x) (f y))
(comm_gg : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → commute (g x) (g y))
(comm_gf : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → 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_4}
[fintype ι]
[decidable_eq ι]
{M : ι → Type u_5}
[Π (i : ι), add_monoid (M i)]
(x : Π (i : ι), M i) :
finset.univ.noncomm_sum (λ (i : ι), pi.single 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 : ι), pi.mul_single 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 (pi.single i x) = ⇑g (pi.single i 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 (pi.mul_single i x) = ⇑g (pi.mul_single i x)) :
f = g