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} [DecidableEq ι] [Zero π] [Fintype ι] [Fintype π] : Fintype (ι →₀ π)

Equations

• Finsupp.fintype = Fintype.ofEquiv (ι → π) Finsupp.equivFunOnFinite.symm

instance Finsupp.infinite_of_left {ι : Type u_1} {π : Type u_2} [Nontrivial π] [Zero π] [Infinite ι] : Infinite (ι →₀ π)

Equations

• (_ : Infinite (ι →₀ π)) = (_ : Infinite (ι →₀ π))

instance Finsupp.infinite_of_right {ι : Type u_1} {π : Type u_2} [Infinite π] [Zero π] [Nonempty ι] : Infinite (ι →₀ π)

Equations

• (_ : Infinite (ι →₀ π)) = (_ : Infinite (ι →₀ π))