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]
:
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]
: