Topological sums and functorial constructions #
Lemmas on the interaction of tprod
, tsum
, HasProd
, HasSum
etc with products, Sigma and Pi
types, MulOpposite
, etc.
Product, Sigma and Pi types #
Alias of HasSum.prodMk
.
Alias of HasProd.prodMk
.
For the statement that tsum
commutes with Finset.sum
,
see Summable.tsum_finsetSum
.
Alias of Summable.tsum_sum
.
For the statement that tsum
commutes with Finset.sum
,
see Summable.tsum_finsetSum
.
Alias of Multipliable.tprod_sum
.
If a function f
on β × γ
has product a
and for each b
the restriction of f
to
{b} × γ
has product g b
, then the function g
has product a
.
If a series f
on β × γ
has sum a
and for each b
the
restriction of f
to {b} × γ
has sum g b
, then the series g
has sum a
.
Alias of Summable.tsum_sigma'
.
Alias of Multipliable.tprod_sigma'
.
Alias of Summable.tsum_prod'
.
Alias of Multipliable.tprod_prod'
.
Alias of Summable.tsum_prod_uncurry
.
Alias of Multipliable.tprod_prod_uncurry
.
Alias of Summable.tsum_comm'
.
Alias of Multipliable.tprod_comm'
.
Alias of Summable.tsum_sigma
.
Alias of Multipliable.tprod_sigma
.
Alias of Summable.tsum_prod
.
Alias of Multipliable.tprod_prod
.
Alias of Summable.tsum_comm
.
Alias of Multipliable.tprod_comm
.