Commit 2022-08-11 16:08 e2ba6de0

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