Erdős problem 1098
Let be a group and be the non-commuting graph, with vertices the elements of and an edge between and if and only if and do not commute, .
Sources
FormalConjectures/ErdosProblems/
1098.lean
Retained formal statement
Neumann [Ne76] noted that if the centre has index then contains no complete subgraph on vertices.
∀ (G : Type u_1) [inst : Group G] [(Subgroup.center G).FiniteIndex], (Erdos1098.nonCommutingGraph G).CliqueFree ((Subgroup.center G).index + 1)SolvedStatement only, no proof