Commit 2020-11-03 09:26 c2b6220c

feat(linear_algebra/matrix): det (reindex e e A) = det A (#4875) This PR includes four flavours of this lemma: det_reindex_self' is the simp lemma that doesn't include the actual term reindex as a subexpression (because that would be already simped away by reindex_apply). det_reindex_self, det_reindex_linear_equiv_self and det_reindex_alg_equiv include their respective function in the lemma statement.