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

Equations

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

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

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

@[simp]

theorem Fintype.card_finsupp (ι : Type u_1) (α : Type u_2) [DecidableEq ι] [Fintype ι] [Zero α] [Fintype α] : Fintype.card (ι →₀ α) = Fintype.card α ^ Fintype.card ι