Commit 2020-06-16 02:35 e0871742

feat(linear_algebra/finite_dimensional): bases given by finsets (#3041) In some cases, it might be more straightforward working with finsets of the vector space instead of indexed types or carrying around a proof of set.finite. Also provide a lemma on equal dimension and basis cardinality lemma that uses a finset basis.