Commit 2021-10-21 18:28 5b72c4ee

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.