K : Type u
V : Type v
inst✝² : Ring K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ↑toNat (Module.rank K { x // x ∈ ⊤ }) = ↑toNat (Module.rank K V)
K : Type u
V : Type v
inst✝² : Ring K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ finrank K { x // x ∈ ⊤ } = finrank K V
unfold finrank
no goals
K : Type u
V : Type v
inst✝² : Ring K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ↑toNat (Module.rank K { x // x ∈ ⊤ }) = ↑toNat (Module.rank K V)
simp [rank_top]