The matrix algebra is a central algebra

theorem Matrix.subalgebraCenter_eq_scalarAlgHom_map {n : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Fintype n] [DecidableEq n] : Subalgebra.center R (Matrix n n A) = Subalgebra.map (scalarAlgHom n R) (Subalgebra.center R A)

instance Algebra.IsCentral.matrix (K : Type u_1) (D : Type u_2) [CommSemiring K] [Semiring D] [Algebra K D] [IsCentral K D] (ι : Type u_3) [Fintype ι] [DecidableEq ι] : IsCentral K (Matrix ι ι D)