mathlib

579cdfe0 - refactor(linear_algebra/affine_space/*): make `affine_basis` more elementary (#18141)

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](https://tqft.net/mathlib4/2023-01-12/all) 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.