Finiteness and infiniteness of finsupp #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Some lemmas on the combination of finsupp, fintype and infinite.
@[protected, instance]
noncomputable
def
finsupp.fintype
{ι : Type u_1}
{π : Type u_2}
[decidable_eq ι]
[has_zero π]
[fintype ι]
[fintype π] :
Equations
@[protected, instance]
def
finsupp.infinite_of_left
{ι : Type u_1}
{π : Type u_2}
[nontrivial π]
[has_zero π]
[infinite ι] :