Documentation

Mathlib.Data.Finsupp.Fintype

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} [inst : DecidableEq ι] [inst : Zero π] [inst : Fintype ι] [inst : Fintype π] :
Fintype (ι →₀ π)
Equations
instance Finsupp.infinite_of_left {ι : Type u_1} {π : Type u_2} [inst : Nontrivial π] [inst : Zero π] [inst : Infinite ι] :
Equations
instance Finsupp.infinite_of_right {ι : Type u_1} {π : Type u_2} [inst : Infinite π] [inst : Zero π] [inst : Nonempty ι] :
Equations