isometryOfOrthonormal — Mathlib

English

The i-th basis vector equals the unit vector in the i-th coordinate.

Русский

i-й вектор базы равен единичному вектору в i-й координате.

LaTeX

$$$$ (\\mathrm{basisFun}_{\\mathbb{R}})=e_i \\text{ for the i-th coordinate}. $$$$

Lean4

/-- The isometry between `ℂ` and a two-dimensional real inner product space given by a basis. -/
def isometryOfOrthonormal (v : OrthonormalBasis (Fin 2) ℝ F) : ℂ ≃ₗᵢ[ℝ] F :=
  Complex.orthonormalBasisOneI.repr.trans v.repr.symm

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