Commit 2026-03-02 18:03 e672f342

View on Github →

feat(GroupTheory): explicit isomorphism between infinite cyclic groups and Z (#35969)

Estimated changes

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

added theorem intEquivOfZMultiplesEqTop_symm_apply_zsmul

added theorem intEquivOfZMultiplesEqTop_symm_self

added theorem intEquivOfZPowersEqTop_symm_self

added theorem mulintEquivOfZPowersEqTop_strictAnti

added theorem mulintEquivOfZPowersEqTop_strictMono

added theorem mulintEquivOfZPowersEqTop_symm_apply_zpow

added theorem zmultiplesHom_bijective

added theorem zpowersHom_bijective