submonoidCenter_eq_scalar_map — Mathlib

English

The center of the matrix ring over a ring R equals the image of the center of R under the scalar embedding.

Русский

Центр кольца матриц над кольцом R равен изображению центра R через скалярное вложение.

LaTeX

$$$$\\mathrm{center}(\\\\mathrm{Matrix}(n,n,R)) = \\\\mathrm{center}(R).\\\\map(\\\\mathrm{scalar}(n)).$$$$

Lean4

theorem submonoidCenter_eq_scalar_map : Submonoid.center (Matrix n n α) = (Submonoid.center α).map (scalar n) :=
  SetLike.coe_injective center_eq_scalar_image

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