Commit 2025-03-01 15:45 d52b8617

feat(GroupTheory/GroupAction/Primitive): lemmas about primitive actions for finite sets (#12053) This PR establishes lemmas about primitive actions for finite types. It also proves the theorem of Rudio : for a primitive action on a finite type, any subset which is neither empty nor full has a translate that contains a given point and avoids another given one.