K✝ : Type u
V✝ : Type v
K V : Type u
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : _root_.Finite K
inst✝ : FiniteDimensional K V
this : IsNoetherian K V := Iff.mpr IsNoetherian.iff_fg inferInstance
⊢ (#V) < ℵ₀
K✝ : Type u
V✝ : Type v
K V : Type u
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : _root_.Finite K
inst✝ : FiniteDimensional K V
⊢ (#V) < ℵ₀
letI : IsNoetherian K V := IsNoetherian.iff_fg.2 inferInstance
K✝ : Type u
V✝ : Type v
K V : Type u
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : _root_.Finite K
inst✝ : FiniteDimensional K V
this : IsNoetherian K V := Iff.mpr IsNoetherian.iff_fg inferInstance
⊢ (#K) ^ Module.rank K V < ℵ₀
K✝ : Type u
V✝ : Type v
K V : Type u
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : _root_.Finite K
inst✝ : FiniteDimensional K V
this : IsNoetherian K V := Iff.mpr IsNoetherian.iff_fg inferInstance
⊢ (#V) < ℵ₀
rw [cardinal_mk_eq_cardinal_mk_field_pow_rank K V]
no goals
K✝ : Type u
V✝ : Type v
K V : Type u
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : _root_.Finite K
inst✝ : FiniteDimensional K V
this : IsNoetherian K V := Iff.mpr IsNoetherian.iff_fg inferInstance
⊢ (#K) ^ Module.rank K V < ℵ₀
exact Cardinal.power_lt_aleph0 (Cardinal.lt_aleph0_of_finite K) (IsNoetherian.rank_lt_aleph0 K V)