K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Set V
inst✝ : Fintype ↑s
hs : LinearIndependent K Subtype.val
this : Module.rank K { x // x ∈ span K s } = (#↑s)
⊢ Module.rank K { x // x ∈ span K s } = ↑(Finset.card (Set.toFinset s))
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Set V
inst✝ : Fintype ↑s
hs : LinearIndependent K Subtype.val
⊢ Module.rank K { x // x ∈ span K s } = ↑(Finset.card (Set.toFinset s))
have : Module.rank K (span K s) = (#s) := rank_span_set hs
no goals
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Set V
inst✝ : Fintype ↑s
hs : LinearIndependent K Subtype.val
this : Module.rank K { x // x ∈ span K s } = (#↑s)
⊢ Module.rank K { x // x ∈ span K s } = ↑(Finset.card (Set.toFinset s))
rwa [Cardinal.mk_fintype, ← Set.toFinset_card] at this