Commit 2021-08-17 13:05 450c2d08

refactor(algebra/algebra/basic): move restrict_scalars into more appropriate files (#8712) This puts:

• submodule.restrict_scalars in submodule.lean since the proofs are all available there, and this is consistent with how linear_map.restrict_scalars is placed. This is almost a copy-paste, but all the R and S variables are swapped to match the existing convention in that file.
• The type alias restrict_scalars is now in its own file. The docstring at the top of the file is entirely new, but the rest is a direct copy and paste. The motivation is primarily to reduce the size of algebra/algebra/basic a little.