coe_center

Mathlib.Algebra.Star.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalStarSubalgebra.coe_center

English

The nonunital subalgebra center of A corresponds to the center of the underlying set A.

Русский

Центр подпалгебры в виде NonUnitalSubalgebra соответствует центру множества A.

LaTeX

$$$\\mathrm{center}\\;R\\;A\\;\\to\\;\\mathrm{NonUnitalSubalgebra}\\;R\\;A = \\mathrm{center}_{R}(A)$$$

Lean4

@[norm_cast]
theorem coe_center : (center R A : Set A) = Set.center A :=
  rfl

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

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

Разделы

Аффилиация

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