The standard orientation of the Euclidean plane

Definition

LeanFormalizations_Geometry_Euclidean_IsometryClassification

by mysticflounder · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrygeometry

This equips the real Euclidean plane with the orientation induced by its standard coordinate basis.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Mathlib

set_option autoImplicit true

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/


open EuclideanGeometry
open scoped Real InnerProductSpace EuclideanSpace

namespace EuclideanGeometry

 
local notation "ℝ²" => EuclideanSpace ℝ (Fin 2)


noncomputable instance : Module.Oriented ℝ ℝ² (Fin 2) :=
  ⟨(EuclideanSpace.basisFun (Fin 2) ℝ).toBasis.orientation⟩

 
local notation "o" => (positiveOrientation : Orientation ℝ ℝ² (Fin 2))

 
local notation "J" => Orientation.rightAngleRotation o


end EuclideanGeometry

View graph