Fix

leanprover-community · Feb 22, 2025 · 2c8cb11 · 2c8cb11
1 parent fd0ba47
commit 2c8cb11
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Analysis/SpecialFunctions/PolarCoord.lean b/Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
@@ -78,7 +78,7 @@ def polarCoord : PartialHomeomorph (ℝ × ℝ) (ℝ × ℝ) where
       (isOpen_ne_fun continuous_snd continuous_const)
   continuousOn_invFun := by fun_prop
   continuousOn_toFun := by
-    refine .prod_mk (by fun_prop) ?_
+    refine .prod (by fun_prop) ?_
     have A : MapsTo Complex.equivRealProd.symm ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
         Complex.slitPlane := by
       rintro ⟨x, y⟩ hxy; simpa only using hxy