Revision #2282 → #2964 · back to history
modifiedExponential covering of the unit circle9ec973b176db
| Field | From #2282 | To #2964 |
|---|
| note | `AddCircle.isCoveringMap_coe` (and `Complex.isCoveringMap_exp`) formalize the universal exponential covering of the circle. | `AddCircle.isCoveringMap_coe` (and `Circle.isCoveringMap_exp`) formalize the universal exponential covering of the circle. |
modifiedUniversal coveringd9fa0b3e75e7
| Field | From #2282 | To #2964 |
|---|
| note | Universal covers are not constructed in Mathlib (no `universalCover` declaration). | Universal covers are not constructed in Mathlib (no `universalCover` declaration for topological spaces). |
addedCoverings are local homeomorphisms (lead)19617b8af0e7
addedCoverings have the homotopy lifting property9b2495ccb747
addedÉtalé space08c9b9949f55