K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : Finset.Nonempty s
lin_ind : LinearIndependent K Subtype.val
card_eq : Finset.card s = finrank K V
⊢ ↑(basisOfLinearIndependentOfCardEqFinrank lin_ind (_ : Fintype.card { x // x ∈ s } = finrank K V)) = Subtype.val
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : Finset.Nonempty s
lin_ind : LinearIndependent K Subtype.val
card_eq : Finset.card s = finrank K V
⊢ ↑(finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq) = Subtype.val
rw [finsetBasisOfLinearIndependentOfCardEqFinrank]
no goals
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : Finset.Nonempty s
lin_ind : LinearIndependent K Subtype.val
card_eq : Finset.card s = finrank K V
⊢ ↑(basisOfLinearIndependentOfCardEqFinrank lin_ind (_ : Fintype.card { x // x ∈ s } = finrank K V)) = Subtype.val
exact Basis.coe_mk _ _