The planar quarter-turn preserves norm

Proved

PlanarRot90Norm

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

crossing-consequencesgeometrypolygonal

The planar quarter-turn operator preserves Euclidean norm: $\|\operatorname{PlanarRot90}(d)\|=\|d\|$ for every planar vector $d$ .

Preamble

import Definitions.Def_PlanarRot90

open Classical
noncomputable section

Formal statement

lemma PlanarRot90Norm (d : EuclideanSpace ℝ (Fin 2)) :
    ‖PlanarRot90 d‖ = ‖d‖ := by sorry

Source