mathlib3

847fc12d - feat(algebra): `submodule.restrict_scalars p R` is `S`-isomorphic to `p` (#8567)

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. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>