mathlib

5b97da63 - feat(ring_theory/matrix_equiv_tensor): matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R) (#3177)

feat(ring_theory/matrix_equiv_tensor): matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R) (#3177) When `A` is an `R`-algebra, matrices over `A` are equivalent (as an algebra) to `A ⊗[R] matrix n n R`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>