Orthogonality of the planar quarter-turn
ProvedPlanarRot90Orthogonalcrossing-consequencesgeometrypolygonal
A planar vector is orthogonal to its quarter-turn: .
Preamble
import Definitions.Def_PlanarRot90 open Classical noncomputable section
Formal statement
lemma PlanarRot90Orthogonal (d : EuclideanSpace ℝ (Fin 2)) :
inner ℝ d (PlanarRot90 d) = 0 := by sorrySource