reindex_linear_equiv

Stream: general

[Johan Commelin]

Recently, reindex_linear_equiv was generalized from being an R-linear equiv between matrix algebras over R to an R-linear equiv between matrix algebras over an R-module A.
Mathematically speaking, this is strictly more general. At the same time

1. I think matrices over a module that isn't an algebra don't show up often in practice. As soon as A is an algebra, one can use restrict_scalars to turn an A-linear equiv into an R-linear one.
2. Unification now cannot guess both R and A, so they have become explicit. But in the common case, R = A, and so unification should have been able to figure it out.

What do people think of the following proposal: the strictly more general version gets renamed reindex_linear_equiv', and the "old" version gets reinstated, defined in terms of the primed version, and points to the primed version in its docstring.

More generally, is there some principal that we can succinctly extract here, and possibly standardize throughout the library? My guess is that this is not possible, and that we need human judgment calls in all the separate cases. But I would love to be wrong there.

[Eric Wieser]

I made this generalization only because it looked like @Filippo A. E. Nuccio (who's currently on vacation) wanted it, and they were building it from scratch rather than using what we had already. Maybe I should have stopped to ask why they wanted it!

[Johan Commelin]

Not that I'm not opposed to the generalization! It's just that I wonder whether it should be the main interface or not.