theorem cardinal_le_aleph0_of_finiteDimensional (K : Type u) (V : Type v) [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] [h : Countable K] : Cardinal.mk V ≤ Cardinal.aleph0

theorem countable_of_finiteDimensional (K : Type u) (V : Type v) [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] [h : Countable K] : Countable V