mathlib

fdace951 - feat(linear_algebra/matrix): generalize some `is_basis.to_matrix` results (#6127)

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.