commProb_closed.toml

id = "commProb_closed"
title = "Commuting probabilities are closed"
test = false
module = "LeanEval.GroupTheory.CommProbClosed"
holes = ["commProb_closed"]
submitter = "Thomas Browning"
notes = "The set of commuting probabilities of finite groups is closed."
source = "https://arxiv.org/abs/2201.09402"
informal_solution = "Neumann's theorem describes the structure of finite groups with bounded below commuting probability. Then pass to subsequences of groups with similar structure."