centralizer_univ

Mathlib.Algebra.Ring.Subsemiring.Basic

URI: https://scilib.ai/kg/mathlib#Subsemiring.centralizer_univ

English

In a semiring R, the centralizer of the universal set Set.univ is exactly the center of R.

Русский

В полусемиринге R центральизатор множества Set.univ совпадает с центром R.

LaTeX

$$$\\operatorname{centralizer}(\\mathrm{Set.univ}) = \\operatorname{center}(R)$$$

Lean4

@[simp]
theorem centralizer_univ {R} [Semiring R] : centralizer Set.univ = center R :=
  SetLike.ext' (Set.centralizer_univ R)

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

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

Разделы

Аффилиация

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