center_toSubring

Mathlib.Algebra.Algebra.Subalgebra.Basic

URI: https://scilib.ai/kg/mathlib#Subalgebra.center_toSubring

English

The underlying subring of the center equals the center regarded as a subring.

Русский

Подкольцо центра совпадает с центром, рассматриваемым как подкольцо.

LaTeX

$$$ (\operatorname{center}(R,A)).toSubring = \operatorname{Subring.center} A $$$

Lean4

@[simp]
theorem center_toSubring (R A : Type*) [CommRing R] [Ring A] [Algebra R A] :
    (center R A).toSubring = Subring.center A :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru