mathlib

c9ae9e67 - chore(linear_algebra/dimension): more same-universe versions of `is_basis.mk_eq_dim` (#4591)

chore(linear_algebra/dimension): more same-universe versions of `is_basis.mk_eq_dim` (#4591) While all the `lift` magic is good for general theory, it is not that convenient for the case when everything is in `Type`. * add `mk_eq_mk_of_basis'`: same-universe version of `mk_eq_mk_of_basis`; * generalize `is_basis.mk_eq_dim''` to any index type in the same universe as `V`, not necessarily `s : set V`; * reorder lemmas to optimize the total length of the proofs; * drop one `finite_dimensional` assumption in `findim_of_infinite_dimensional`.