feat(LinearAlgebra/Matrix/Reindex): AddEquiv and RingEquiv

[SnirBroshi]

We had Matrix.reindex bundled as a LinearEquiv and an AlgEquiv,
and this bundles it as an AddEquiv and a RingEquiv.

---

[github-actions]

PR summary 043e9e0413

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ reindexAddEquiv
+ reindexRingEquiv

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[eric-wieser]

For the other reindex equivs we seem to write this manually; does it produce a matching lemma?

[SnirBroshi]

The generated *_apply lemmas match modulo simpNF (the RHS of reindexLinearEquiv_apply/reindexAlgEquiv_apply isn't simpNF because of reindex_apply, not sure why the linter allows them).

simps also generates *_symm_apply lemmas which look good, but it doesn't generate unapplied *_symm lemmas like the other equivs have, nor Equiv.refl/Equiv.trans lemmas which look nice.

Although everyone is missing a DFunLike.coe lemma (including reindex itself), which might fix everything.

wdyt?

[themathqueen]

The RHS doesn't need to be in simpNF form. If foo_apply simplifies to _ = reindex, then it'll end also end up simplifying further using the reindex API.

I like the *_symm lemmas being a simp more than *_symm_apply. You can have both though, if you want?

Please also add *_symm lemmas, and Equiv.refl, and the rest.

[themathqueen]

there's also toEquiv_reindexAddEquiv that's missing. And same with the rest, (i.e., toAddEquiv_reindexRingEquiv, etc)