We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 50eb251 commit 8ba3f94Copy full SHA for 8ba3f94
Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
@@ -203,4 +203,4 @@ theorem Circle.isAddQuotientCoveringMap_exp :
203
theorem Circle.isCoveringMap_exp : IsCoveringMap exp := isAddQuotientCoveringMap_exp.isCoveringMap
204
205
lemma isLocalHomeomorph_circleExp : IsLocalHomeomorph Circle.exp :=
206
- homeomorphCircle'.isLocalHomeomorph.comp (isLocalHomeomorph_coe (2 * π))
+ Circle.isCoveringMap_exp.isLocalHomeomorph
0 commit comments