mathlib

5b72c4ee - feat(linear_algebra/quotient): `S.restrict_scalars.quotient` is `S.quotient` (#9535)

feat(linear_algebra/quotient): `S.restrict_scalars.quotient` is `S.quotient` (#9535) This PR adds a more general module instance on submodule quotients, in order to show that `(S.restrict_scalars R).quotient` is equivalent to `S.quotient`. If we decide this instance is not a good idea, I can write it instead as `S.quotient.restrict_scalars`, but that is a bit less convenient to work with. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>