Theorem AddCircle.finite_torsion

Modification history

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

2025-05-12 14:24

Mathlib/Topology/Instances/AddCircle.lean

chore(Topology/Instances/AddCircle): golf and little lemmas (#23236)

Added AddCircle.finite_torsion View on Github →