Countable modules

instance 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 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 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

@[deprecated Countable.of_moduleFinite (since := "2026-10-24")]

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

Alias of Countable.of_moduleFinite.

@[deprecated Uncountable.of_moduleFinite (since := "2026-10-24")]

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

Alias of Uncountable.of_moduleFinite.