Erdős problem 1098

Let $G$ be a group and $\Gamma=\Gamma(G)$ be the non-commuting graph, with vertices the elements of $G$ and an edge between $g$ and $h$ if and only if $g$ and $h$ do not commute, $gh\neq hg$ .

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1098.lean

Retained formal statement2 of 4

Neumann [Ne76] proved that $\Gamma$ contains no infinite complete subgraph if and only if the centre of the group has finite index.

FormalConjectures/ErdosProblems/1098.leanErdos1098.erdos_1098.variants.center_finiteIndex2 linesExact file

1∀ (G : Type u_1) [inst : Group G],2  (∀ (s : Set G), (Erdos1098.nonCommutingGraph G).IsClique s → s.Finite) ↔ (Subgroup.center G).FiniteIndex

SolvedStatement only, no proof