English
Let E be a 2-dimensional real inner product space with an orientation o. For any nonzero x, the basis produced by the right-angle rotation is the ordered pair (x, Jx); in particular, its coordinate column equals the vector [x, Jx].
Русский
Пусть E — ориентированное двумерное вещественное вещественно-векторное пространство с ориентированием o. Для любого ненулевого вектора x базис, порождаемый вращением на 90 градусов, является упорядоченным базисом (x, Jx); в частности, его координатная колонка равна вектору [x, Jx].
LaTeX
$$$\\operatorname{coe}\\big(o.basisRightAngleRotation(x,hx)\\big) = \\!\\left[ x, \\; Jx \\right]$$$
Lean4
@[simp]
theorem coe_basisRightAngleRotation (x : E) (hx : x ≠ 0) : ⇑(o.basisRightAngleRotation x hx) = ![x, J x] :=
coe_basisOfLinearIndependentOfCardEqFinrank _ _