English
For every z ∈ ℂ, polarCoord z = (|z|, Arg z).
Русский
Для каждого z ∈ ℂ полярная координата z равна (|z|, Arg z).
LaTeX
$$$$ \mathrm{Complex}.\mathrm{polarCoord}(z) = (|z|, \arg z) \quad (z \in \mathbb{C}). $$$$
Lean4
/-- The polar coordinates open partial homeomorphism in `ℂ`, mapping `r (cos θ + I * sin θ)` to
`(r, θ)`. It is a homeomorphism between `ℂ - ℝ≤0` and `(0, +∞) × (-π, π)`. -/
protected noncomputable def polarCoord : OpenPartialHomeomorph ℂ (ℝ × ℝ) :=
equivRealProdCLM.toHomeomorph.transOpenPartialHomeomorph polarCoord