commutator_eq_bot_iff_center_eq_top

English

The commutator subgroup is trivial (equal to ⊥) if and only if the center equals the whole group (center G = ⊤).

Русский

Коммутаторная подгруппа тривиальна тогда и только тогда, когда центр всей группы равен всей группе (центр G = ⊤).

LaTeX

$$$ \\operatorname{commutator}(G) = \\bot \\;\\;\\Longleftrightarrow\\;\\; \\operatorname{center}(G) = \\top $$$

Lean4

theorem commutator_eq_bot_iff_center_eq_top : commutator G = ⊥ ↔ Subgroup.center G = ⊤ := by
  simp [commutator, Subgroup.commutator_eq_bot_iff_le_centralizer]

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