Finiteness and infiniteness of Finsupp
#
Some lemmas on the combination of Finsupp
, Fintype
and Infinite
.
noncomputable instance
Finsupp.fintype
{ι : Type u_1}
{π : Type u_2}
[inst : DecidableEq ι]
[inst : Zero π]
[inst : Fintype ι]
[inst : Fintype π]
:
Equations
- Finsupp.fintype = Fintype.ofEquiv (ι → π) (Equiv.symm Finsupp.equivFunOnFinite)
instance
Finsupp.infinite_of_left
{ι : Type u_1}
{π : Type u_2}
[inst : Nontrivial π]
[inst : Zero π]
[inst : Infinite ι]
: