coe_basisRightAngleRotation — Mathlib

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 _ _

Похожие утверждения