cyclic_center_quotient_of_card_eq_prime_sq

English

If |G| = p^2 for a prime p, then G/Z(G) is cyclic.

Русский

Если |G| = p^2 для простого p, то фактор-группа G/Z(G) циклична.

LaTeX

$$$|G| = p^2 \implies G/Z(G) \text{ is cyclic.}$$$

Lean4

/-- The quotient by the center of a group of cardinality `p ^ 2` is cyclic. -/
theorem cyclic_center_quotient_of_card_eq_prime_sq (hG : Nat.card G = p ^ 2) : IsCyclic (G ⧸ center G) :=
  by
  apply isCyclic_of_card_dvd_prime (p := p)
  rw [← mul_dvd_mul_iff_left (NeZero.ne p), ← sq, ← hG, ← (center G).card_mul_index]
  apply mul_dvd_mul_right
  rcases card_center_eq_prime_pow hG zero_lt_two with ⟨k, hk0, hk⟩
  rw [hk]
  exact dvd_pow_self p hk0.ne'

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