oangle — Mathlib

English

The oriented angle from x to y is defined as the argument of the Kahler form associated to the orientation o.

Русский

Ориентированный угол от вектора x к вектору y определяется как аргумент формы Kahler, связанной с ориентированием o.

LaTeX

$$$\mathrm{oangle}(x,y) = \arg\bigl( \kappa_o(x,y) \bigr)$$$

Lean4

/-- The oriented angle from `x` to `y`, modulo `2 * π`. If either vector is 0, this is 0.
See `InnerProductGeometry.angle` for the corresponding unoriented angle definition. -/
def oangle (x y : V) : Real.Angle :=
  Complex.arg (o.kahler x y)

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