Commit 2021-02-11 11:50 fdace951

feat(linear_algebra/matrix): generalize some is_basis.to_matrix results (#6127) This PR contains some changes to the lemmas involving is_basis.to_matrix, allowing the bases involved to differ in their index type. Although you can prove there exists an equiv between those types, it's easier to not have to transport along that equiv. The PR also generalizes linear_map.to_matrix_id to a form with two different bases, linear_map.to_matrix_id_eq_basis_to_matrix. Marking the second as simp means the first can be proved automatically, hence the removal of simp on that one.