mathlib

e2ba6de0 - feat(linear_algebra/span, matrix, finite_dimensional): new lemmas (#16006)

feat(linear_algebra/span, matrix, finite_dimensional): new lemmas (#16006) + Introduce `submodule.supr_span` and deduce `submodule.supr_eq_span` from it. + Use supr_span to prove that the range of `matrix.to_lin' M` is spanned by column vectors of `M`. + Show the rank of a finite set in a vector space is at most the cardinality of the indexing type (`finrank_range_le_card`), so in order to show the set is linearly independent, it suffices to prove the reverse inequality (`linear_independent_iff_card_le_finrank_span`). Spinoff of [Zulip question](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/more.20linear.20algebra/near/292630550)