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.
Co-authored-by: Scott Morrison scott.morrison@gmail.com
mathlib
e0871742 - feat(linear_algebra/finite_dimensional): bases given by finsets (#3041)
