Theorems · Definition · geometry

EuclideanGeometry.oangle

{V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [NormedAddTorsor V P] →
            [hd2 : Fact (Module.finrank ℝ V = 2)] → [Module.Oriented ℝ V (Fin 2)] → P → P → P → Real.Angle

The oriented angle at p₂ between the line segments to p₁ and p₃, modulo 2 * π. If either of those points equals p₂, this is 0. See EuclideanGeometry.angle for the corresponding unoriented angle definition.

Defined in

Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Cited by

188 results in Mathlib

Foundations

Depth 252 from the axioms, rests on 7,313 definitions · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorFactModule.Oriented