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] proved that contains no infinite complete subgraph if and only if the centre of the group has finite index.
∀ (G : Type u_1) [inst : Group G], (∀ (s : Set G), (Erdos1098.nonCommutingGraph G).IsClique s → s.Finite) ↔ (Subgroup.center G).FiniteIndexSolvedStatement only, no proof