basisRightAngleRotation — Mathlib

English

For nonzero x ∈ E, the pair (x, J x) forms a basis of E (i.e., spans E and is linearly independent).

Русский

Для не нулевого вектора x ∈ E пара (x, J x) образует базис пространства E.

LaTeX

$$$\\text{span}_{\\\\mathbb{R}}\\{x, J x\\} = E \\quad\\text{и}\\quad x, J x \\text{ линейно независимы}$$$

Lean4

/-- For a nonzero vector `x` in an oriented two-dimensional real inner product space `E`,
`![x, J x]` forms an (orthogonal) basis for `E`. -/
def basisRightAngleRotation (x : E) (hx : x ≠ 0) : Basis (Fin 2) ℝ E :=
  @basisOfLinearIndependentOfCardEqFinrank ℝ _ _ _ _ _ _ _ ![x, J x]
    (linearIndependent_of_ne_zero_of_inner_eq_zero (fun i => by fin_cases i <;> simp [hx])
      (by
        intro i j hij
        fin_cases i <;> fin_cases j <;> simp_all))
    (@Fact.out (finrank ℝ E = 2)).symm

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