K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
ι : Type w
h : Basis ι K V
this : IsNoetherian K V
⊢ ↑(finrank K V) = (#ι)
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
ι : Type w
h : Basis ι K V
⊢ ↑(finrank K V) = (#ι)
haveI : IsNoetherian K V := iff_fg.2 inferInstance
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
ι : Type w
h : Basis ι K V
this✝ : IsNoetherian K V
this : Fintype ι
⊢ ↑(finrank K V) = (#ι)
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
ι : Type w
h : Basis ι K V
this : IsNoetherian K V
⊢ ↑(finrank K V) = (#ι)
haveI : Fintype ι := fintypeBasisIndex h
no goals
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
ι : Type w
h : Basis ι K V
this✝ : IsNoetherian K V
this : Fintype ι
⊢ ↑(finrank K V) = (#ι)
rw [Cardinal.mk_fintype, finrank_eq_card_basis h]