Theorem mulintEquivOfZPowersEqTop_strictMono

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_strictMono View on Github →