mathlib3

2b84c4c6 - feat(linear_algebra/matrix/basis): add matrix basis change formula (#9280)

feat(linear_algebra/matrix/basis): add matrix basis change formula (#9280) We add `basis_to_matrix_mul_linear_map_to_matrix_mul_basis_to_matrix`, the formula for the change of basis.