Injectivity of a map defined via basis.constr

Stream: new members

[Brendan Seamas Murphy]

Say I have vector spaces V, W over a field k, a basis b : basis ι k V, and a family of vectors f : ι →W. I can get a linear map T := b.constr f from this data and it should be that function.injective ⇑T ↔ linear_independent k f. Is there a lemma that states this? I can't find it

[Adam Topaz]

We do have docs#linear_independent_iff_injective_total which would make it easy, but I do agree that we should have a lemma using bases.

[Adam Topaz]

Note that constr is defined via finsupp.total see docs#basis.constr_def