oangle — Mathlib

English

For complex numbers w and z, the oriented angle is given by the argument of the product of the conjugate of w and z: oangle w z = arg( conj(w) z ).

Русский

Для комплексных чисел w и z ориентированный угол равен аргументу произведения сопряженного числа w на z: oangle w z = arg( conj(w) z ).

LaTeX

$$$ \text{Complex.oangle}(w,z) = \text{Complex.arg}(\overline{w} \cdot z) $$$

Lean4

@[simp]
protected theorem _root_.Complex.oangle (w z : ℂ) : Complex.orientation.oangle w z = Complex.arg (conj w * z) := by
  simp [oangle, mul_comm z]

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