one_mem_centralizer

Mathlib.Algebra.Group.Center

URI: https://scilib.ai/kg/mathlib#Set.one_mem_centralizer

English

The identity element 1 belongs to the center in a monoid or semigroup with unit.

Русский

Единица 1 принадлежит центру в моноиде или полугруппе с единицей.

LaTeX

$$$ 1 \in \mathrm{center}(M) $$$

Lean4

@[to_additive (attr := simp) zero_mem_addCentralizer]
theorem one_mem_centralizer : (1 : M) ∈ centralizer S := by simp [mem_centralizer_iff]

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

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

Разделы

Аффилиация

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