Commit 2020-10-13 06:30 c9ae9e67

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.