subringCenter_eq_scalar_map — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem subringCenter_eq_scalar_map [Ring R] : Subring.center (Matrix n n R) = (Subring.center R).map (scalar n) :=
  SetLike.coe_injective center_eq_scalar_image

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