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.
- (2,3)-generation of groups
- Coprime generation
- Eulerian polynomials of groups
- Generation by elements of prime-power order
- Generator number of almost simple groups
- Rank of a group generated by two subgroups
- Spread of a group
- Two-generated direct powers of simple groups
TheoremSubgroup generated by a symmetric set#✓fully proved
Subgroup.closure_eq_iUnion_pow
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
Sources
- 2310.10246 D01 (main.tex:146).
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.