Theorem AddCircle.finite_torsion

Modification history

2025-12-22 22:40
Mathlib/Topology/Instances/AddCircle/Defs.lean
feat: covering maps from properly discontinuous actions and discrete subgroups (#7596)
Modified AddCircle.finite_torsionView on Github →
2025-12-10 18:38
Mathlib/Topology/Instances/AddCircle/Defs.lean
feat(Topology/AddCircle): remove `0 < p` condition from `finite_torsion` (#32691)
Modified AddCircle.finite_torsionView on Github →
2025-05-12 14:24
Mathlib/Topology/Instances/AddCircle.lean
chore(Topology/Instances/AddCircle): golf and little lemmas (#23236)
Added AddCircle.finite_torsionView on Github →