K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s : Set V
inst✝¹ : Nonempty ↑s
inst✝ : Fintype ↑s
lin_ind : LinearIndependent K Subtype.val
card_eq : Finset.card (Set.toFinset s) = finrank K V
⊢ ↑(basisOfLinearIndependentOfCardEqFinrank lin_ind (_ : Fintype.card ↑s = finrank K V)) = Subtype.val
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s : Set V
inst✝¹ : Nonempty ↑s
inst✝ : Fintype ↑s
lin_ind : LinearIndependent K Subtype.val
card_eq : Finset.card (Set.toFinset s) = finrank K V
⊢ ↑(setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = Subtype.val
rw [setBasisOfLinearIndependentOfCardEqFinrank]
no goals
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s : Set V
inst✝¹ : Nonempty ↑s
inst✝ : Fintype ↑s
lin_ind : LinearIndependent K Subtype.val
card_eq : Finset.card (Set.toFinset s) = finrank K V
⊢ ↑(basisOfLinearIndependentOfCardEqFinrank lin_ind (_ : Fintype.card ↑s = finrank K V)) = Subtype.val
exact Basis.coe_mk _ _