mathlib

97781b9a - chore(linear_algebra/std_basis): move std_basis to a new file (#6020)

chore(linear_algebra/std_basis): move std_basis to a new file (#6020) linear_algebra/basic is _very_ long. This reduces its length by about 5%. Authorship of the std_basis stuff seems to come almost entirely from 10a586b1d82098af32e13c8d8448696022132f17. None of the lemmas have changed, and the variables are kept in exactly the same order as before.