norm_polarCoord_symm — Mathlib

English

The norm of the inverse polar map equals the absolute value of the radius coordinate: for p ∈ ℝ × ℝ, ‖Complex.polarCoord.symm(p)‖ = |p.1|.

Русский

Норма обратной полярной карты равна абсолютному значению радиусной координаты: для p ∈ ℝ × ℝ верно ‖Complex.polarCoord.symm(p)‖ = |p_1|.

LaTeX

$$$\|\mathrm{Complex.polarCoord.symm}(p)\| = |p_1|\quad (p \in \mathbb{R}^2).$$$

Lean4

theorem norm_polarCoord_symm (p : ℝ × ℝ) : ‖Complex.polarCoord.symm p‖ = |p.1| := by simp

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