polarCoord_symm_apply — Mathlib

English

The inverse polar coordinate map sends p = (r, θ) to r( cos θ + i sin θ ).

Русский

Обратная полярная карта отправляет p=(r,θ) в r( cos θ + i sin θ ).

LaTeX

$$$$ \mathrm{Complex}.\mathrm{polarCoord}.symm(p) = p_1 \big( \cos p_2 + i \sin p_2 \big). $$$$

Lean4

@[simp]
protected theorem polarCoord_symm_apply (p : ℝ × ℝ) :
    Complex.polarCoord.symm p = p.1 * (Real.cos p.2 + Real.sin p.2 * Complex.I) := by
  simp [Complex.polarCoord, equivRealProdCLM_symm_apply, mul_add, mul_assoc]

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