mathlib

0f085b98 - chore(linear_algebra/finite_dimensional): rename `of_finite_basis` (#4562)

chore(linear_algebra/finite_dimensional): rename `of_finite_basis` (#4562) * rename `of_finite_basis` to `of_fintype_basis`; * add new `of_finite_basis` assuming that the domain the basis is a `finite` set; * allow `s : finset ι` and any function `s → V` in `of_finset_basis`.