Commit 2025-05-06 06:29 3fbf14e0

View on Github →

feat(GroupTheory/Cyclic): formula for the card & index of kernel & range of powMonoidHom on a cyclic group (#23461) We prove formula for the cardinal and index of the kernel and range of powMonoidHom : x ↦ x ^ d on a finite cyclic group.

Estimated changes

Modified Mathlib/GroupTheory/Index.lean

added theorem Subgroup.index_range

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

added theorem IsCyclic.card_powMonoidHom_ker

added theorem IsCyclic.card_powMonoidHom_range

added theorem IsCyclic.index_powMonoidHom_ker

added theorem IsCyclic.index_powMonoidHom_range

added theorem orderOf_eq_card_of_zpowers_eq_top