Big operators and fin
#
Some results about products and sums over the type fin
.
The most important results are the induction formulas fin.prod_univ_cast_succ
and fin.prod_univ_succ
, and the formula fin.prod_const
for the product of a
constant function. These results have variants for sums instead of products.
A sum of a function f : fin 0 → β
is 0
because fin 0
is empty
A product of a function f : fin 0 → β
is 1
because fin 0
is empty
A product of a function f : fin (n + 1) → β
over all fin (n + 1)
is the product of f x
, for some x : fin (n + 1)
times the remaining product
A product of a function f : fin (n + 1) → β
over all fin (n + 1)
is the product of f 0
plus the remaining product
A product of a function f : fin (n + 1) → β
over all fin (n + 1)
is the product of f (fin.last n)
plus the remaining product