The standard orientation on ℂ.

This had previously been in LinearAlgebra.Orientation, but keeping it separate results in a significant import reduction.

noncomputable def Complex.orientation : Orientation ℝ ℂ (Fin 2)

The standard orientation on ℂ.

Equations

• Complex.orientation = Basis.orientation Complex.basisOneI