Fintype instances for pi types #
Given for all
a : α a finset
t a of
δ a, then one can define the
Fintype.piFinset t of all functions taking values in
t a for all
a. This is the
Finset.pi where the base finset is
univ (but formally they are not the same, as
there is an additional condition
i ∈ Finset.univ in the
- One or more equations did not get rendered due to their size.
A dependent product of fintypes, indexed by a fintype, is a fintype.