Commit 2021-05-25 17:19 8078ecad

feat(linear_algebra): det (M ⬝ N ⬝ M') = det N, where M' is an inverse of M (#7633) This is an important step towards showing the determinant of linear_map.to_matrix does not depend on the choice of basis.

The main difficulty is allowing the two indexing types of M to be (a priori) different. They are in bijection though (using basis.index_equiv from #7631), so using reindex_linear_equiv we can turn everything into square matrices and apply the "usual" proof.