center_toSubsemiring

Mathlib.Algebra.Ring.Subring.Basic

URI: https://scilib.ai/kg/mathlib#Subring.center_toSubsemiring

English

The center of R, viewed as a Subring, is equal to the center of R as a Subsemiring.

Русский

Центр R, рассматриваемый как подкольцо, равен центру R как подполу.

LaTeX

$$(center R).toSubsemiring = Subsemiring.center R$$

Lean4

@[simp]
theorem center_toSubsemiring : (center R).toSubsemiring = Subsemiring.center R :=
  rfl

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

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

Разделы

Аффилиация

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