commutative_of_card_eq_prime_sq

Mathlib.GroupTheory.PGroup

URI: https://scilib.ai/kg/mathlib#IsPGroup.commutative_of_card_eq_prime_sq

← MathLib Explorer

English

If |G| = p^2 for a prime p, then G is abelian (same as commGroupOfCardEqPrimeSq).

Русский

Если |G| = p^2, то G абелева.

LaTeX

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

Lean4

/-- A group of order `p ^ 2` is commutative. See also `IsPGroup.commGroupOfCardEqPrimeSq`
for the `CommGroup` instance. -/
theorem commutative_of_card_eq_prime_sq (hG : Nat.card G = p ^ 2) : ∀ a b : G, a * b = b * a :=
  (commGroupOfCardEqPrimeSq hG).mul_comm

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru