subalgebraCenter_eq_scalarAlgHom_map

English

The center of the matrix algebra M_n(A) over R coincides with the image of the center of A under the scalar embedding.

Русский

центр матричной алгебры M_n(A) над R совпадает с образом центра A через скалярное вложение.

LaTeX

$$$\\operatorname{center}_R(\\mathrm{Matrix}\\;n\\;n\\;A) = \\operatorname{center}_R(A).map(\\mathrm{scalarAlgHom}\\;n\\;R)$$$

Lean4

theorem subalgebraCenter_eq_scalarAlgHom_map :
    Subalgebra.center R (Matrix n n A) = (Subalgebra.center R A).map (scalarAlgHom n R) :=
  SetLike.coe_injective center_eq_scalar_image

Похожие утверждения