instCommRingSubtypeMemCenter

Mathlib.Algebra.Algebra.Subalgebra.Basic

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

English

If A is a ring, the center of A is a commutative ring.

Русский

Если A — кольцо, то центр A образует коммутативное кольцо.

LaTeX

$$$\text{center}(R,A) \text{ is a CommRing when } A \text{ is a ring}$$$

Lean4

instance {A : Type*} [Ring A] [Algebra R A] : CommRing (center R A) :=
  inferInstanceAs (CommRing (Subring.center A))

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

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

Разделы

Аффилиация

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