feat: Countable.of_module_finite (leanprover-community#34994)

Co-authored-by: bwangpj <70694994+bwangpj@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Author: bwangpj

Mathlib/LinearAlgebra/Countable.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Data.Finsupp.Encodable
 public import Mathlib.Data.Set.Countable
 public import Mathlib.LinearAlgebra.Finsupp.LinearCombination
+public import Mathlib.RingTheory.Finiteness.Defs
 
 /-!
 # Countable modules
@@ -29,4 +30,14 @@ instance {ι : Type*} [Countable R] [Countable ι] (v : ι → M) :
       (fun c : (ι →₀ R) => c.sum fun i _ => (c i) • v i)))
   exact fun _ h => Finsupp.mem_span_range_iff_exists_finsupp.mp (SetLike.mem_coe.mp h)
 
+theorem Countable.of_moduleFinite [Countable R] [Module.Finite R M] : Countable M := by
+  obtain ⟨n, s, h⟩ := Module.Finite.exists_fin (R := R) (M := M)
+  rw [← Set.countable_univ_iff]
+  have : Countable (Submodule.span R (Set.range s)) := inferInstance
+  rwa [h] at this
+
+theorem Uncountable.of_moduleFinite [hM : Uncountable M] [Module.Finite R M] : Uncountable R := by
+  by_contra!
+  exact (uncountable_iff_not_countable _).mp hM <| Countable.of_moduleFinite (R := R)
+
 end Finsupp