Commit 2024-12-20 16:26 2a41753e

View on Github →

feat(GroupTheory/SpecificGroups/Cyclic): Add isCyclic_of_injective (#20103) This PR adds isCyclic_of_injective and uses it to golf Subgroup.isCyclic_of_le.

Estimated changes

modified theorem Subgroup.isCyclic_of_le
added theorem isCyclic_of_injective