Countable modules

instance Finsupp.instCountableSubtypeMemSubmoduleSpanRange {M : Type u_1} {R : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} [Countable R] [Countable ι] (v : ι → M) : Countable ↥(Submodule.span R (Set.range v))

If R is countable, then any R-submodule spanned by a countable family of vectors is countable.

theorem Finsupp.Countable.of_moduleFinite {M : Type u_1} {R : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Countable R] [Module.Finite R M] : Countable M

theorem Finsupp.Uncountable.of_moduleFinite {M : Type u_1} {R : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [hM : Uncountable M] [Module.Finite R M] : Uncountable R