commGroupOfCyclicCenterQuotient — Mathlib

English

A group is commutative if the quotient by the center is cyclic.

Русский

Группа коммутативна, если фактор по центру цикличен.

LaTeX

$$commGroupOfCyclicCenterQuotient (f : G →* G') (hf : ker f ≤ center G) : CommGroup G$$

Lean4

/-- A group is commutative if the quotient by the center is cyclic. -/
@[to_additive /-- A group is commutative if the quotient by the center is cyclic. -/
    ]
def commGroupOfCyclicCenterQuotient [IsCyclic G'] (f : G →* G') (hf : f.ker ≤ center G) : CommGroup G :=
  { show Group G by infer_instance with mul_comm := commutative_of_cyclic_center_quotient f hf }

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