Def AddCircle.openPartialHomeomorphCoe

Modification history

2025-10-02 09:10
Mathlib/Topology/Instances/AddCircle/Defs.lean
chore: rename PartialHomeomorph to OpenPartialHomeomorph (#29113) …
Added AddCircle.openPartialHomeomorphCoeView on Github →