isMulCommutative

Mathlib.GroupTheory.Subgroup.Center

URI: https://scilib.ai/kg/mathlib#Subgroup.center.isMulCommutative

English

The center is abelian: any two elements in the center commute with each other.

Русский

Центр абелев: любые два элемента центра commute между собой.

LaTeX

$$∀ x,y ∈ Z(G), xy = yx$$

Lean4

instance isMulCommutative : IsMulCommutative (center G) :=
  ⟨⟨fun a b => Subtype.ext (b.2.comm a).symm⟩⟩

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

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

Разделы

Аффилиация

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