Generation of groups

Minimal and special generating sets: generator numbers of almost simple and soluble groups, (2,3)-generation, generation by elements of prime-power order, spread, coprime generation, two-generated direct powers, Eulerian functions and probabilistic generation.

TheoremSubgroup generated by a symmetric set#✓fully proved

Let \(G\) be a group and let \(X \subseteq G\) satisfy \(X^{-1} = X\), where \(X^{-1} = \{x^{-1} : x \in X\}\). Then the subgroup of \(G\) generated by \(X\) equals \(\bigcup_{n \in \mathbb{N}} X^n\), where \(X^0 = \{1\}\) and \(X^{n+1} = X^n X = \{yx : y \in X^n,\ x \in X\}\).

theorem closure_eq_iUnion_pow (hX : X⁻¹ = X) :
    (Subgroup.closure X : Set G) = ⋃ n : ℕ, X ^ n
Sources
  • 2310.10246 D01 (main.tex:146).

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.