Commit 2024-11-28 14:24 28d3cb71
View on Github →feat(GroupTheory/SpecificGroups/Cyclic): Cardinality of automorphism group (#19180)
This PR computes the cardinality of the automorphism group of a cyclic group. This is useful when paired with the N/C theorem in PR #19006.
I added a new file to avoid adding extra imports to Data/ZMod/Basic.lean.