K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : Module.rank K V = 0
this : FiniteDimensional K V
⊢ ⊥ = ⊤
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : Module.rank K V = 0
⊢ ⊥ = ⊤
haveI : FiniteDimensional _ _ := finiteDimensional_of_rank_eq_zero h
case h
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : Module.rank K V = 0
this : FiniteDimensional K V
⊢ finrank K { x // x ∈ ⊥ } = finrank K V
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : Module.rank K V = 0
this : FiniteDimensional K V
⊢ ⊥ = ⊤
apply eq_top_of_finrank_eq
no goals
case h
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : Module.rank K V = 0
this : FiniteDimensional K V
⊢ finrank K { x // x ∈ ⊥ } = finrank K V
rw [finrank_bot, finrank_eq_zero_of_rank_eq_zero h]