Rotation of a linear combination in the planar quarter-turn basis

Proved

PlanarRot90LinearCombination

by xuanji · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebraplanar-geometry

For a vector $u$ in the Euclidean plane, let $\operatorname{Rot}_{90}$ denote the quarter-turn rotation. Applying the rotation to a linear combination of the basis vectors $u$ and $\operatorname{Rot}_{90}(u)$ gives

\operatorname{Rot}_{90}igl(Au+B\operatorname{Rot}_{90}(u)igr) =-Bu+A\operatorname{Rot}_{90}(u).

This is the coordinate rule for the quarter-turn operator in the oriented two-dimensional basis generated by $u$ . It is used to rewrite rotated cone expressions as scalar coefficient identities.

Preamble

import Definitions.Def_PlanarRot90

open Classical
noncomputable section

Formal statement

theorem PlanarRot90LinearCombination (u : EuclideanSpace ℝ (Fin 2)) (A B : ℝ) :
    PlanarRot90 (A • u + B • PlanarRot90 u) =
      (-B) • u + A • PlanarRot90 u := by sorry

Source

https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/PlanarRot90LinearCombination.lean#L1-L10

View graph