le_centralizer

Mathlib.GroupTheory.Subgroup.Centralizer

URI: https://scilib.ai/kg/mathlib#Subgroup.le_centralizer

English

If H is multiplicatively commutative, then H is contained in its centralizer: H ≤ centralizer(H).

Русский

Если H коммутативна относительно умножения, то H ⊆ centralizer(H).

LaTeX

$$[h : IsMulCommutative H] : H ≤ centralizer(H)$$

Lean4

@[to_additive]
theorem le_centralizer [h : IsMulCommutative H] : H ≤ centralizer H :=
  le_centralizer_iff_isMulCommutative.mpr h

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

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

Разделы

Аффилиация

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