feat(linear_algebra/basis): repr_support_of_mem_span (#14504)

This lemma states that if a vector is in the span of a subset of the basis vectors, only this subset of basis vectors will be used in its `repr` representation.



Co-authored-by: Alexander Bentkamp <a.bentkamp@vu.nl>

src/linear_algebra/basis.lean

@@ -146,6 +146,13 @@ lemma mem_span_repr_support {ι : Type*} (b : basis ι R M) (m : M) :
   m ∈ span R (b '' (b.repr m).support) :=
 (finsupp.mem_span_image_iff_total _).2 ⟨b.repr m, (by simp [finsupp.mem_supported_support])⟩
 
+lemma repr_support_subset_of_mem_span {ι : Type*}
+  (b : basis ι R M) (s : set ι) {m : M} (hm : m ∈ span R (b '' s)) : ↑(b.repr m).support ⊆ s :=
+begin
+  rcases (finsupp.mem_span_image_iff_total _).1 hm with ⟨l, hl, hlm⟩,
+  rwa [←hlm, repr_total, ←finsupp.mem_supported R l]
+end
+
 end repr
 
 section coord