mathlib3

63c8d333 - feat(linear_algebra/matrix/reindex): generalize reindex_linear_equiv to operate on an arbitrary ring (#8159)

feat(linear_algebra/matrix/reindex): generalize reindex_linear_equiv to operate on an arbitrary ring (#8159) This changes `reindex_linear_equiv eₘ eₙ : matrix m m R ≃ₗ[R] matrix n n R` to `reindex_linear_equiv R A eₘ eₙ : matrix m m A ≃ₗ[R] matrix n n A`, which both works for a larger range of types, and eliminates the need for type ascriptions that was previously caused by the implicitness of `R`. We cannot yet make the same generalization for `reindex_alg_equiv` as the `algebra R (matrix m m A)` structure implied by `algebra R A` is not in mathlib yet.