K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : ℕ
h : Module.rank K V = ↑n
⊢ ↑n < ℵ₀
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : ℕ
h : Module.rank K V = ↑n
⊢ FiniteDimensional K V
rw [FiniteDimensional, ← IsNoetherian.iff_fg, IsNoetherian.iff_rank_lt_aleph0, h]
no goals
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : ℕ
h : Module.rank K V = ↑n
⊢ ↑n < ℵ₀
exact nat_lt_aleph0 n