feat(linear_algebra/matrix/reindex): add some lemmas (#7963)
From LTE
Added lemmas `reindex_linear_equiv_trans`, `reindex_linear_equiv_comp`, `reindex_linear_equiv_comp_apply`, `reindex_linear_equiv_one` and `mul_reindex_linear_equiv_mul_one` needed in LTE.
Co-authored-by: Filippo Nuccio <nuccio@cluster18-math.univ-lyon1.fr>
Co-authored-by: Filippo A. E. Nuccio <65080144+faenuccio@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
