Results about "big operations" over a Fintype
, and consequent
results about cardinalities of certain types.
Implementation note #
This content had previously been in Data.Fintype.Basic
, but was moved here to avoid
requiring Algebra.BigOperators
(and hence many other imports) as a
dependency of Fintype
.
However many of the results here really belong in Algebra.BigOperators.Group.Finset
and should be moved at some point.
If a sum of a Finset
of a subsingleton type has a given
value, so do the terms in that sum.
If a product of a Finset
of a subsingleton type has a given
value, so do the terms in that product.
This lemma is specifically designed to be used backwards, whence the specialisation to Fin n
as the indexing type doesn't matter in practice. The more general forward direction lemma here is
Fintype.card_piFinset
.
This lemma is specifically designed to be used backwards, whence the specialisation to Fin n
as the indexing type doesn't matter in practice. The more general forward direction lemma here is
Fintype.card_pi
.
The number of dependent maps f : Π j, s j
for which the i
component is a
is the product
over all j ≠ i
of (s j).card
.
Note that this is just a composition of easier lemmas, but there's some glue missing to make that smooth enough not to need this lemma.
It is equivalent to sum a function over fin n
or finset.range n
.
It is equivalent to compute the product of a function over Fin n
or Finset.range n
.
The sum over a product type equals the sum of fiberwise sums.
For rewriting in the reverse direction, use Fintype.sum_prod_type'
.
The product over a product type equals the product of the fiberwise products. For rewriting
in the reverse direction, use Fintype.prod_prod_type'
.
The sum over a product type equals the sum of fiberwise sums.
For rewriting in the reverse direction, use Fintype.sum_prod_type
.
The product over a product type equals the product of the fiberwise products. For rewriting
in the reverse direction, use Fintype.prod_prod_type
.
An uncurried version of Finset.sum_prod_type_right
An uncurried version of Finset.prod_prod_type_right
.