Matrix algebra tensor compatibility

This file restores an upstream matrix/tensor equivalence in the opposite direction.

def matrixEquivTensor' (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] [Fintype n] [DecidableEq n] : Matrix n n A ≃ₐ[A] TensorProduct R A (Matrix n n R)

Matrix algebras over A as scalar extension from matrices over R.

Equations

• matrixEquivTensor' n R A = (AlgEquiv.ofRingEquiv ⋯).symm

@[simp]

theorem matrixEquivTensor'_symm_apply (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] [Fintype n] [DecidableEq n] (a : A) (m : Matrix n n R) : (matrixEquivTensor' n R A).symm (a ⊗ₜ[R] m) = a • m.map ⇑(algebraMap R A)