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

Modified Mathlib.lean

Modified Mathlib/Algebra/Squarefree/Basic.lean

modified theorem Squarefree.eq_zero_or_one_of_pow_of_not_isUnit

modified theorem Squarefree.of_mul_left

added theorem Squarefree.pow_dvd_of_pow_dvd

modified theorem Squarefree.squarefree_of_dvd

Created Mathlib/GroupTheory/SpecificGroups/ZGroup.lean

added theorem IsZGroup.of_injective

added theorem IsZGroup.of_squarefree