Conjugacy classes
Conjugacy classes of groups as a structural invariant: class sizes and breadth, the class number, commuting probability, Thompson's conjecture on class sizes, products of conjugacy classes, and relations between class sizes and group structure; class sizes of p-groups go to Finite p-groups, and character-theoretic class arguments to Characters of finite groups.
- Breadth of a finite group
- Centralizers of maximal order
- Class number of a finite group
- Largest conjugacy class of perfect groups
- p-parts of conjugacy class sizes
- Products of conjugacy classes in alternating groups
- Thompson's conjecture on conjugacy class sizes
- Torsion-free groups with three conjugacy classes
TheoremThe set of commuting probabilities is closed#●ready to prove
MathlibExt.GroupTheory.CommProbClosedWanted.GroupTheory.commProb_closed
Let \(\Pr(G)\) denote the commuting probability of a group \(G\): \(\Pr(G) = |\{(x, y) \in G \times G : xy = yx\}| / |G|^2\) if \(G\) is finite, and \(\Pr(G) = 0\) if \(G\) is infinite. Then the set \(\{\Pr(G) : G \text{ a group}\}\) is a closed subset of \(\mathbb{R}\).
public theorem_wanted commProb_closed : IsClosed ({p : ℝ | ∃ (G : Type) (hG : Group G), @commProb G hG.toMul = p})Sources
Sources
- https://arxiv.org/abs/2201.09402. Problem
commProb_closedof the lean-eval benchmark.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.