Products (respectively, sums) over a finset or a multiset. #
The regular Finset.prod
and Multiset.prod
require [CommMonoid α]
.
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.noncommProd
, requiring a proof of commutativity of held termsMultiset.noncommProd
, requiring a proof of commutativity of held terms
Implementation details #
While List.prod
is defined via List.foldl
, noncommProd
is defined via
Multiset.foldr
for neater proofs and definitions. By the commutativity assumption,
the two must be equal.
TODO: Tidy up this file by using the fact that the submonoid generated by commuting
elements is commutative and using the Finset.prod
versions of lemmas to prove the noncommProd
version.
Fold of a s : Multiset α
with f : α → β → β
, given a proof that LeftCommutative f
on all elements x ∈ s
.
Equations
- One or more equations did not get rendered due to their size.
Fold of a s : Multiset α
with an associative op : α → α → α
, given a proofs that op
is commutative on all elements x ∈ s
.
Equations
- Multiset.noncommFold op s comm = Multiset.noncommFoldr op s (_ : ∀ (x : α), x ∈ { x | x ∈ s } → ∀ (y : α), y ∈ { x | x ∈ s } → x ≠ y → ∀ (b : α), op x (op y b) = op y (op x b))
Sum of a s : Multiset α
with [AddMonoid α]
, given a proof that +
commutes
on all elements x ∈ s
.
Equations
- Multiset.noncommSum s comm = Multiset.noncommFold (fun x x_1 => x + x_1) s comm 0
Equations
- (_ : IsAssociative α fun x x_1 => x + x_1) = (_ : IsAssociative α fun x x_1 => x + x_1)
Product of a s : Multiset α
with [Monoid α]
, given a proof that *
commutes
on all elements x ∈ s
.
Equations
- Multiset.noncommProd s comm = Multiset.noncommFold (fun x x_1 => x * x_1) s comm 1
Proof used in definition of `Finset.noncommProd
Sum of a s : Finset α
mapped with f : α → β
with [AddMonoid β]
,
given a proof that +
commutes on all elements f x
for x ∈ s
.
Equations
- Finset.noncommSum s f comm = Multiset.noncommSum (Multiset.map f s.val) (_ : Set.Pairwise { x | x ∈ Multiset.map f s.val } AddCommute)
Product of a s : Finset α
mapped with f : α → β
with [Monoid β]
,
given a proof that *
commutes on all elements f x
for x ∈ s
.
Equations
- Finset.noncommProd s f comm = Multiset.noncommProd (Multiset.map f s.val) (_ : Set.Pairwise { x | x ∈ Multiset.map f s.val } Commute)
The non-commutative version of finset.sum_union
The non-commutative version of Finset.prod_union
The non-commutative version of Finset.sum_add_distrib
The non-commutative version of Finset.prod_mul_distrib