Commit 2021-07-05 10:29 63c8d333

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.