Commit 2023-01-12 09:11 579cdfe0

refactor(linear_algebra/affine_space/*): make affine_basis more elementary (#18141) In the linear algebra development of mathlib, basis is more elementary than finite_dimension, and matrix results are not imported to the main theory until determinants. This PR changes the structure of the affine linear algebra development to match that. I think this is worth doing in any case, but my motivation is to decrease the length of the current longest chain in mathlib and particularly the length of the chain to analysis.convex.specific_functions, which is imported by measure theory. This actually only reduces those chains in length slightly, since there is a second nearly-as-long path from data.set.finite to analysis.convex.specific_functions which passes through topology, metric spaces, and normed spaces, rather than through linear algebra, noetherian rings, free modules, and matrix theory. But that one can be studied later.