polarCoord — Mathlib

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

Похожие утверждения