center_eq_top

Mathlib.GroupTheory.Subgroup.Center

URI: https://scilib.ai/kg/mathlib#CommGroup.center_eq_top

← MathLib Explorer

English

In a commutative group, the center is the whole group: Z(G) = G.

Русский

В коммутативной группе центр — вся группа: Z(G) = G.

LaTeX

$$$G\text{ commutative} \Rightarrow Z(G) = G$$$

Lean4

theorem _root_.CommGroup.center_eq_top {G : Type*} [CommGroup G] : center G = ⊤ :=
  by
  rw [eq_top_iff']
  intro x
  rw [Subgroup.mem_center_iff]
  intro y
  exact mul_comm y x

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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