subsemigroupCenter_eq_scalar_map — Mathlib

English

The center of the matrix subring equals the image of the center of the base ring via the scalar embedding.

Русский

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

LaTeX

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

Lean4

theorem subsemigroupCenter_eq_scalar_map :
    Subsemigroup.center (Matrix n n α) = (Subsemigroup.center α).map (scalar n).toMulHom :=
  SetLike.coe_injective center_eq_scalar_image

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