mathlib

8b630df3 - feat(ring_theory/matrix_algebra): drop commutativity assumption (#3351)

feat(ring_theory/matrix_algebra): drop commutativity assumption (#3351) Remove the unnecessary assumption that `A` is commutative in `matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R)`. (This didn't cause a problem for Cayley-Hamilton, but @alexjbest and Bassem Safieldeen [realised it's not necessary](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Tensor.20product.20of.20matrices).) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>