commGroupOfCenterEqTop — Mathlib

English

A group is commutative if and only if its center equals the whole group.

Русский

Группа является абелевой тогда и только тогда, когда ее центр равен всей группе.

LaTeX

$$$Z(G) = G \iff G \text{ is abelian}$$$

Lean4

/-- A group is commutative if the center is the whole group -/
def _root_.Group.commGroupOfCenterEqTop (h : center G = ⊤) : CommGroup G :=
  { ‹Group G› with
    mul_comm := by
      rw [eq_top_iff'] at h
      intro x y
      apply Subgroup.mem_center_iff.mp _ x
      exact h y }

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