mathlib3

bd38c5ff - chore(linear_algebra): move `is_basis_std_basis` to `std_basis.lean` (#6054)

chore(linear_algebra): move `is_basis_std_basis` to `std_basis.lean` (#6054) This is a follow-up to #6020 which moved `std_basis` to a new file: now move results from `basis.lean` to that same file. CC @eric-wieser Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>