Commit 2021-08-09 15:47 847fc12d

feat(algebra): submodule.restrict_scalars p R is S-isomorphic to p (#8567) To be more precise, turning p : submodule S M into an R-submodule gives the same module structure as turning it into a type and adding a module structure.