mathlib documentation


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 π] :
fintype →₀ π)
@[protected, instance]
def finsupp.infinite_of_left {ι : Type u_1} {π : Type u_2} [nontrivial π] [has_zero π] [infinite ι] :
@[protected, instance]
def finsupp.infinite_of_right {ι : Type u_1} {π : Type u_2} [infinite π] [has_zero π] [nonempty ι] :