Theorem AddCircle.card_torsion_le_of_isSMulRegular

Modification history

2025-12-22 22:40
Mathlib/Topology/Instances/AddCircle/Defs.lean
feat: covering maps from properly discontinuous actions and discrete subgroups (#7596)
Added AddCircle.card_torsion_le_of_isSMulRegularView on Github →