commGroupOfCardEqPrimeSq — Mathlib

English

A group of order p^2 is abelian.

Русский

Группа порядка p^2 абелева.

LaTeX

$$$|G| = p^2 \Rightarrow G \text{ is abelian.}$$$

Lean4

/-- A group of order `p ^ 2` is commutative. See also `IsPGroup.commutative_of_card_eq_prime_sq`
for just the proof that `∀ a b, a * b = b * a` -/
def commGroupOfCardEqPrimeSq (hG : Nat.card G = p ^ 2) : CommGroup G :=
  @commGroupOfCyclicCenterQuotient _ _ _ _ (cyclic_center_quotient_of_card_eq_prime_sq hG) _
    (QuotientGroup.ker_mk' (center G)).le

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