Theorem AddCircle.injOn_coe_Ico

Modification history

2026-11-10 11:56

Mathlib/Topology/Instances/AddCircle/Defs.lean

feat(Topology/Instances/AddCircle): `Infinite (AddCircle p)` for a densely ordered group (#45575)

Added AddCircle.injOn_coe_Ico View on Github →