Commit 2022-05-14 08:16 79bc06bf

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.