Theorem mulintEquivOfZPowersEqTop_symm_apply_zpow

Modification history

2026-03-02 18:03
Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
feat(GroupTheory): explicit isomorphism between infinite cyclic groups and Z (#35969)
Added mulintEquivOfZPowersEqTop_symm_apply_zpowView on Github →