mathlib3

79bc06bf - feat(linear_algebra/matrix/to_lin): equivalence via right multiplication (#13870)

feat(linear_algebra/matrix/to_lin): equivalence via right multiplication (#13870) A very partial generalization of `linear_algebra/matrix/to_lin` to non-commutative rings. This is far from a complete refactor of the file; it just adds enough for what I need in representation theory immediately. I've left an extensive note explaining what should be done in a later refactor, but I don't want to have to do this all at once. See discussion on [zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/matrices). Co-authored-by: Scott Morrison <scott.morrison@gmail.com>