mathlib

c2b6220c - feat(linear_algebra/matrix): `det (reindex e e A) = det A` (#4875)

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 `simp`ed 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. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>