mathlib3

450c2d08 - refactor(algebra/algebra/basic): move restrict_scalars into more appropriate files (#8712)

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.