mathlib3

86add5ce - refactor(linear_algebra/matrix/rank): remove `decidable_eq` arguments (#18800)

refactor(linear_algebra/matrix/rank): remove `decidable_eq` arguments (#18800) `matrix.to_lin' M` is just `matrix.vec_mul_lin M` with an unused decidability argument. We're a bit close to the tide to risk attempting to do a global replacement, so this just: * Refactors some lemmas about `matrix.to_lin'` to be first proven about `matrix.vec_mul_lin` * Changes `matrix.rank` to be defined in terms of the latter.