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.

Equations

• ⋯ = ⋯