mathlib3

baab5d30 - refactor(data/matrix): reverse the direction of `matrix.minor_mul_equiv` (#10657)

refactor(data/matrix): reverse the direction of `matrix.minor_mul_equiv` (#10657) In #10350 this change was proposed, since we apparently use that backwards way more than we use it forwards. We also change `reindex_linear_equiv_mul`, which is similarly much more popular backwards than forwards. Closes: #10638