Finite p-groups

Groups of prime-power order: composition series, Frattini subgroups and Φ-extensions, special, powerful, metacyclic and Camina p-groups, conjugacy class sizes of p-groups, generalized quaternion groups, coclass and rank analogues, derived length bounds, and orders of automorphism groups of p-groups only when the p-group structure is the point.

• 2-groups in which normal closures determine conjugacy
• Abelian subgroups of p-groups
• Camina groups
• Coclass and rank of p-groups
• Cohomology of p-groups and the Frattini subgroup
• Composition series of finite p-groups
• Conjugacy class sizes of p-groups
• Derived and Frattini subgroups of p-groups
• Derived length of p-groups via 2-generator subgroups
• Generating p-groups by elements of equal order
• Large automorphism groups of p-groups
• Normal subgroups of exponent p in p-groups
• Orders of 2-groups of bounded abelian rank
• p-groups with special maximal subgroups
• Partitions of p-groups
• Powerful p-groups
• Φ-extensions of p-groups

DefinitionGeneralized quaternion group#✓fully proved

A group \(P\) is a generalized quaternion group if, for some natural number \(k \ge 1\), it is isomorphic to the quaternion group \(Q_{2^{k+2}} = \langle a, x \mid a^{2^{k+1}} = 1,\ x^2 = a^{2^k},\ x^{-1} a x = a^{-1} \rangle\) of order \(2^{k+2}\). Thus \(P\) has order \(8\), \(16\), \(32\) or some larger power of \(2\).

def IsGeneralizedQuaternion (P : Type*) [Group P] : Prop :=
  ∃ k : ℕ, 1 ≤ k ∧ Nonempty (P ≃* QuaternionGroup (2 ^ k))

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.