[Merged by Bors] - feat(LinearAlgebra/LinearIndependent): add linearIndependent_iff_finset_linearIndependent

[acmepjz]

A family is linearly independent if and only if all of its finite subfamily is linearly independent.

---

[riccardobrasca]

Is linearIndependent_finset_map_embedding_subtype one direction of (a special case of) your lemma? It seems so... in this case can you erase linearIndependent_finset_map_embedding_subtype?

[acmepjz]

Is linearIndependent_finset_map_embedding_subtype one direction of (a special case of) your lemma? It seems so... in this case can you erase linearIndependent_finset_map_embedding_subtype?

I think you're right. but in linearIndependent_finset_map_embedding_subtype the index set Finset.map (Embedding.subtype s) t has type Finset M, whereas my version it's just t which is of type Finset s. In the following linearIndependent_bounded_of_finset_linearIndependent_bounded it uses such convention (namely the input argument of it uses Finset M). I haven't figured out how to use my result to prove it.

[riccardobrasca]

Is linearIndependent_finset_map_embedding_subtype one direction of (a special case of) your lemma? It seems so...

Yeah, linearIndependent_finset_map_embedding_subtype is stated for sets, the results that connect linear independence for sets and types are later, so it seems complicated to use you result. We can maybe add the covers of linearIndependent_finset_map_embedding_subtype, but in my opinion the API for sets should be avoided.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style