Theorems · Definition · geometry

EuclideanGeometry.o

{R : Type u_3} →
  {inst : CommSemiring R} →
    {inst_1 : PartialOrder R} →
      {inst_2 : IsStrictOrderedRing R} →
        {M : Type u_4} →
          {inst_3 : AddCommMonoid M} →
            {inst_4 : Module R M} → {ι : Type u_5} → [self : Module.Oriented R M ι] → Orientation R M ι

A fixed choice of positive orientation of Euclidean space ℝ²

Defined in

Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Cited by

48 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Module.Oriented