Commit 2024-11-13 17:52 a4f79d69

View on Github →

feat(GroupTheory/SpecificGroups/ZGroup): Predicate for groups whose Sylow subgroups are all cyclic (#18575) This PR adds a predicate stating that all Sylow subgroups of G are cyclic (for instance, when G has squarefree order). Ultimately, the goal is to show that any such group is a semidirect product of two cyclic groups.

Estimated changes