def EuclideanGeometry.«termℝ³» : Lean.ParserDescr

Equations

• EuclideanGeometry.«termℝ³» = Lean.ParserDescr.node `EuclideanGeometry.«termℝ³» 1024 (Lean.ParserDescr.symbol "ℝ³")

noncomputable instance Module.orientedEuclideanSpaceFinThree : Oriented ℝ (EuclideanSpace ℝ (Fin 3)) (Fin 3)

The standard basis gives us a preferred orientation in ℝ³.

Note: when upstreaming this to Mathlib (and generalizing to Fin n) one must be careful to avoid an instance diamond with IsEmpty.Orientation. Presumably this can be avoided by assuming [NeZero n].

Equations

• Module.orientedEuclideanSpaceFinThree = { positiveOrientation := (Pi.basisFun ℝ (Fin 3)).orientation }

instance fact_finrank_euclideanSpace_fin_three : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin 3)) = 3)

Three dimensional euclidean space is three-dimensional.