Commit 2021-02-10 21:01 bce1cb3e

feat(linear_algebra/matrix): lemmas for reindex({_linear,_alg}_equiv)? (#6153) This PR contains a couple of simp lemmas for reindex and its bundled equivs. Namely, it adds reindex_refl (reindexing along the identity map is the identity), and reindex_apply (the same as coe_reindex, but no λ i j on the RHS, which makes it more useful for rw'ing.) The previous reindex_apply is renamed coe_reindex for disambiguation.