refactor(linear_algebra/quotient_module): avoid using type class inference for setoids

[ChrisHughes24]

Continuation of #212 . Avoid using type class inference for quotient modules, and introduce a version of quotient.mk specifically for quotient modules, whose output type is quotient β s rather than quotient (quotient_rel s), which should help type class inference
TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

For reviewers: code review check list