Finiteness and infiniteness of Finsupp

Some lemmas on the combination of Finsupp, Fintype and Infinite.

ink

noncomputable instance Finsupp.fintype {ι : Type u_1} {π : Type u_2} [inst : DecidableEq ι] [inst : Zero π] [inst : Fintype ι] [inst : Fintype π] : Fintype (ι →₀ π)

Equations

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

ink

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

Equations

• @Finsupp.infinite_of_left = @Finsupp.infinite_of_left.proof_1

ink

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

Equations

• @Finsupp.infinite_of_right = @Finsupp.infinite_of_right.proof_1