centralizer_eq_top_iff_subset

Mathlib.GroupTheory.Subgroup.Centralizer

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

← MathLib Explorer

English

centralizer(s) = G iff s ⊆ Z(G).

Русский

centralizer(s) = G тогда и только тогда, когда s ⊆ Z(G).

LaTeX

$$centralizer(s) = G \iff s \subseteq Z(G)$$

Lean4

@[to_additive (attr := simp)]
theorem centralizer_eq_top_iff_subset {s : Set G} : centralizer s = ⊤ ↔ s ⊆ center G :=
  SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset

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

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

Разделы

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

Аффилиация

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